scilib documentation

core / init.default

source

Imports

init.cc_lemmas
init.classical
init.coe
init.control.combinators
init.core
init.function
init.funext
init.logic
init.meta.feature_search
init.meta.float
init.meta.well_founded_tactics
init.propext
init.util
init.version
init.wf

Imported by

adsorption.BETInfinite
adsorption.langmuir_kinetics
dimensional_analysis.basic
dimensional_analysis.buckingham_pi
math.antideriv
math.deriv
math.infinite_series
math.rpow
molecular_mechanics.lennard_jones
molecular_mechanics.translation_invariance_LJ
physics.kinematic_equations
thermodynamics.basic
thermodynamics.boyles_law
data.buffer
data.dlist
system.io
system.io_interface
system.random
algebra.abs
algebra.add_torsor
algebra.algebra.basic
algebra.algebra.bilinear
algebra.algebra.equiv
algebra.algebra.hom
algebra.algebra.operations
algebra.algebra.pi
algebra.algebra.prod
algebra.algebra.restrict_scalars
algebra.algebra.subalgebra.basic
algebra.algebra.subalgebra.tower
algebra.algebra.tower
algebra.associated
algebra.big_operators.associated
algebra.big_operators.basic
algebra.big_operators.fin
algebra.big_operators.finprod
algebra.big_operators.finsupp
algebra.big_operators.intervals
algebra.big_operators.multiset.basic
algebra.big_operators.multiset.lemmas
algebra.big_operators.nat_antidiagonal
algebra.big_operators.option
algebra.big_operators.order
algebra.big_operators.pi
algebra.big_operators.ring
algebra.big_operators.ring_equiv
algebra.bounds
algebra.char_p.basic
algebra.char_p.invertible
algebra.char_p.two
algebra.char_zero.defs
algebra.char_zero.infinite
algebra.char_zero.lemmas
algebra.char_zero.quotient
algebra.covariant_and_contravariant
algebra.direct_sum.basic
algebra.direct_sum.finsupp
algebra.direct_sum.module
algebra.divisibility.basic
algebra.divisibility.units
algebra.euclidean_domain.basic
algebra.euclidean_domain.defs
algebra.euclidean_domain.instances
algebra.field.basic
algebra.field.defs
algebra.field.opposite
algebra.free_monoid.basic
algebra.gcd_monoid.basic
algebra.gcd_monoid.finset
algebra.gcd_monoid.multiset
algebra.geom_sum
algebra.group.basic
algebra.group.commutator
algebra.group.commute
algebra.group.conj
algebra.group.defs
algebra.group.inj_surj
algebra.group.opposite
algebra.group.order_synonym
algebra.group.pi
algebra.group.prod
algebra.group.semiconj
algebra.group.type_tags
algebra.group.ulift
algebra.group.units
algebra.group.with_one.defs
algebra.group_power.basic
algebra.group_power.lemmas
algebra.group_power.order
algebra.group_power.ring
algebra.group_ring_action.basic
algebra.group_ring_action.subobjects
algebra.group_with_zero.basic
algebra.group_with_zero.commute
algebra.group_with_zero.defs
algebra.group_with_zero.divisibility
algebra.group_with_zero.inj_surj
algebra.group_with_zero.power
algebra.group_with_zero.semiconj
algebra.group_with_zero.units.basic
algebra.group_with_zero.units.lemmas
algebra.hom.aut
algebra.hom.commute
algebra.hom.embedding
algebra.hom.equiv.basic
algebra.hom.equiv.units.basic
algebra.hom.equiv.units.group_with_zero
algebra.hom.group
algebra.hom.group_action
algebra.hom.group_instances
algebra.hom.iterate
algebra.hom.non_unital_alg
algebra.hom.ring
algebra.hom.units
algebra.indicator_function
algebra.invertible
algebra.modeq
algebra.module.algebra
algebra.module.basic
algebra.module.big_operators
algebra.module.equiv
algebra.module.hom
algebra.module.linear_map
algebra.module.opposites
algebra.module.pi
algebra.module.prod
algebra.module.submodule.basic
algebra.module.submodule.bilinear
algebra.module.submodule.lattice
algebra.module.submodule.pointwise
algebra.module.ulift
algebra.monoid_algebra.basic
algebra.monoid_algebra.division
algebra.monoid_algebra.support
algebra.ne_zero
algebra.opposites
algebra.order.absolute_value
algebra.order.archimedean
algebra.order.field.basic
algebra.order.field.canonical.basic
algebra.order.field.canonical.defs
algebra.order.field.defs
algebra.order.field.inj_surj
algebra.order.field.power
algebra.order.floor
algebra.order.group.abs
algebra.order.group.bounds
algebra.order.group.defs
algebra.order.group.inj_surj
algebra.order.group.instances
algebra.order.group.min_max
algebra.order.group.order_iso
algebra.order.group.type_tags
algebra.order.group.units
algebra.order.hom.basic
algebra.order.invertible
algebra.order.kleene
algebra.order.module
algebra.order.monoid.basic
algebra.order.monoid.cancel.basic
algebra.order.monoid.cancel.defs
algebra.order.monoid.canonical.defs
algebra.order.monoid.defs
algebra.order.monoid.lemmas
algebra.order.monoid.min_max
algebra.order.monoid.nat_cast
algebra.order.monoid.order_dual
algebra.order.monoid.prod
algebra.order.monoid.type_tags
algebra.order.monoid.units
algebra.order.monoid.with_top
algebra.order.monoid.with_zero.basic
algebra.order.monoid.with_zero.defs
algebra.order.nonneg.field
algebra.order.nonneg.floor
algebra.order.nonneg.ring
algebra.order.pi
algebra.order.positive.ring
algebra.order.ring.abs
algebra.order.ring.canonical
algebra.order.ring.char_zero
algebra.order.ring.defs
algebra.order.ring.inj_surj
algebra.order.ring.lemmas
algebra.order.ring.with_top
algebra.order.smul
algebra.order.sub.canonical
algebra.order.sub.defs
algebra.order.sub.with_top
algebra.order.to_interval_mod
algebra.order.with_zero
algebra.order.zero_le_one
algebra.parity
algebra.periodic
algebra.polynomial.big_operators
algebra.punit_instances
algebra.quotient
algebra.regular.basic
algebra.regular.smul
algebra.ring.add_aut
algebra.ring.aut
algebra.ring.basic
algebra.ring.commute
algebra.ring.comp_typeclasses
algebra.ring.defs
algebra.ring.divisibility
algebra.ring.equiv
algebra.ring.fin
algebra.ring.idempotents
algebra.ring.inj_surj
algebra.ring.opposite
algebra.ring.pi
algebra.ring.prod
algebra.ring.regular
algebra.ring.semiconj
algebra.ring.ulift
algebra.ring.units
algebra.smul_with_zero
algebra.star.basic
algebra.star.big_operators
algebra.star.module
algebra.star.order
algebra.star.pi
algebra.star.pointwise
algebra.star.prod
algebra.star.self_adjoint
algebra.star.star_alg_hom
algebra.star.subalgebra
algebra.star.unitary
algebra.support
analysis.asymptotics.asymptotic_equivalent
analysis.asymptotics.asymptotics
analysis.asymptotics.theta
analysis.calculus.conformal.normed_space
analysis.calculus.cont_diff
analysis.calculus.cont_diff_def
analysis.calculus.deriv.add
analysis.calculus.deriv.basic
analysis.calculus.deriv.comp
analysis.calculus.deriv.inv
analysis.calculus.deriv.inverse
analysis.calculus.deriv.linear
analysis.calculus.deriv.mul
analysis.calculus.deriv.polynomial
analysis.calculus.deriv.pow
analysis.calculus.deriv.prod
analysis.calculus.deriv.slope
analysis.calculus.deriv.zpow
analysis.calculus.extend_deriv
analysis.calculus.fderiv.add
analysis.calculus.fderiv.basic
analysis.calculus.fderiv.bilinear
analysis.calculus.fderiv.comp
analysis.calculus.fderiv.equiv
analysis.calculus.fderiv.linear
analysis.calculus.fderiv.mul
analysis.calculus.fderiv.prod
analysis.calculus.fderiv.restrict_scalars
analysis.calculus.formal_multilinear_series
analysis.calculus.inverse
analysis.calculus.iterated_deriv
analysis.calculus.lhopital
analysis.calculus.local_extr
analysis.calculus.mean_value
analysis.calculus.tangent_cone
analysis.complex.basic
analysis.complex.circle
analysis.complex.conformal
analysis.complex.isometry
analysis.complex.real_deriv
analysis.convex.basic
analysis.convex.combination
analysis.convex.function
analysis.convex.hull
analysis.convex.jensen
analysis.convex.normed
analysis.convex.segment
analysis.convex.slope
analysis.convex.star
analysis.convex.strict
analysis.convex.strict_convex_space
analysis.convex.topology
analysis.convex.uniform
analysis.inner_product_space.basic
analysis.locally_convex.balanced_core_hull
analysis.locally_convex.basic
analysis.locally_convex.bounded
analysis.normed.field.basic
analysis.normed.field.unit_ball
analysis.normed.group.add_circle
analysis.normed.group.add_torsor
analysis.normed.group.ball_sphere
analysis.normed.group.basic
analysis.normed.group.completion
analysis.normed.group.hom
analysis.normed.group.infinite_sum
analysis.normed.group.pointwise
analysis.normed.group.quotient
analysis.normed.group.seminorm
analysis.normed.mul_action
analysis.normed.order.basic
analysis.normed_space.add_torsor
analysis.normed_space.affine_isometry
analysis.normed_space.banach
analysis.normed_space.basic
analysis.normed_space.bounded_linear_maps
analysis.normed_space.completion
analysis.normed_space.conformal_linear_map
analysis.normed_space.continuous_linear_map
analysis.normed_space.finite_dimension
analysis.normed_space.linear_isometry
analysis.normed_space.multilinear
analysis.normed_space.operator_norm
analysis.normed_space.pointwise
analysis.normed_space.ray
analysis.normed_space.riesz_lemma
analysis.normed_space.star.basic
analysis.normed_space.units
analysis.seminorm
analysis.special_functions.complex.arg
analysis.special_functions.complex.log
analysis.special_functions.complex.log_deriv
analysis.special_functions.exp
analysis.special_functions.exp_deriv
analysis.special_functions.log.basic
analysis.special_functions.log.deriv
analysis.special_functions.pow.asymptotics
analysis.special_functions.pow.complex
analysis.special_functions.pow.continuity
analysis.special_functions.pow.deriv
analysis.special_functions.pow.nnreal
analysis.special_functions.pow.real
analysis.special_functions.trigonometric.angle
analysis.special_functions.trigonometric.basic
analysis.special_functions.trigonometric.deriv
analysis.special_functions.trigonometric.inverse
analysis.specific_limits.basic
analysis.specific_limits.normed
combinatorics.composition
combinatorics.partition
control.applicative
control.basic
control.bifunctor
control.equiv_functor
control.functor
control.monad.basic
control.traversable.basic
control.traversable.derive
control.traversable.instances
control.traversable.lemmas
data.bool.basic
data.bool.set
data.bracket
data.complex.basic
data.complex.exponential
data.complex.module
data.countable.basic
data.countable.defs
data.dfinsupp.basic
data.dlist.basic
data.enat.basic
data.enat.lattice
data.fin.basic
data.fin.interval
data.fin.tuple.basic
data.fin.vec_notation
data.fin_enum
data.finite.basic
data.finite.card
data.finite.defs
data.finite.set
data.finset.basic
data.finset.card
data.finset.fin
data.finset.fold
data.finset.image
data.finset.lattice
data.finset.locally_finite
data.finset.n_ary
data.finset.nat_antidiagonal
data.finset.noncomm_prod
data.finset.option
data.finset.order
data.finset.pairwise
data.finset.pi
data.finset.pointwise
data.finset.powerset
data.finset.preimage
data.finset.prod
data.finset.sigma
data.finset.sort
data.finset.sum
data.finsupp.antidiagonal
data.finsupp.basic
data.finsupp.defs
data.finsupp.fin
data.finsupp.indicator
data.finsupp.multiset
data.finsupp.order
data.finsupp.to_dfinsupp
data.fintype.basic
data.fintype.big_operators
data.fintype.card
data.fintype.fin
data.fintype.lattice
data.fintype.list
data.fintype.option
data.fintype.perm
data.fintype.pi
data.fintype.powerset
data.fintype.prod
data.fintype.sigma
data.fintype.sort
data.fintype.sum
data.fintype.units
data.fintype.vector
data.fun_like.basic
data.fun_like.embedding
data.fun_like.equiv
data.int.basic
data.int.bitwise
data.int.cast.basic
data.int.cast.defs
data.int.cast.field
data.int.cast.lemmas
data.int.cast.prod
data.int.char_zero
data.int.div
data.int.dvd.basic
data.int.gcd
data.int.interval
data.int.least_greatest
data.int.lemmas
data.int.modeq
data.int.order.basic
data.int.order.lemmas
data.int.order.units
data.int.parity
data.int.succ_pred
data.int.units
data.is_R_or_C.basic
data.list.basic
data.list.big_operators.basic
data.list.big_operators.lemmas
data.list.chain
data.list.count
data.list.cycle
data.list.dedup
data.list.defs
data.list.duplicate
data.list.fin_range
data.list.forall2
data.list.infix
data.list.join
data.list.lattice
data.list.lex
data.list.min_max
data.list.nat_antidiagonal
data.list.nodup
data.list.nodup_equiv_fin
data.list.of_fn
data.list.pairwise
data.list.perm
data.list.permutation
data.list.prime
data.list.prod_sigma
data.list.range
data.list.rotate
data.list.sort
data.list.sublists
data.list.tfae
data.list.zip
data.matrix.basic
data.matrix.basis
data.matrix.block
data.matrix.notation
data.matrix.pequiv
data.matrix.rank
data.mllist
data.multiset.antidiagonal
data.multiset.basic
data.multiset.bind
data.multiset.dedup
data.multiset.finset_ops
data.multiset.fold
data.multiset.lattice
data.multiset.nat_antidiagonal
data.multiset.nodup
data.multiset.pi
data.multiset.powerset
data.multiset.range
data.multiset.sort
data.multiset.sum
data.mv_polynomial.basic
data.mv_polynomial.comm_ring
data.mv_polynomial.equiv
data.mv_polynomial.rename
data.mv_polynomial.variables
data.nat.basic
data.nat.bits
data.nat.bitwise
data.nat.cast.basic
data.nat.cast.defs
data.nat.cast.field
data.nat.cast.prod
data.nat.choose.basic
data.nat.choose.cast
data.nat.choose.sum
data.nat.count
data.nat.factorial.basic
data.nat.factorial.cast
data.nat.factorization.basic
data.nat.factors
data.nat.gcd.basic
data.nat.interval
data.nat.lattice
data.nat.log
data.nat.modeq
data.nat.multiplicity
data.nat.order.basic
data.nat.order.lemmas
data.nat.pairing
data.nat.parity
data.nat.part_enat
data.nat.periodic
data.nat.pow
data.nat.prime
data.nat.prime_fin
data.nat.set
data.nat.size
data.nat.sqrt
data.nat.succ_pred
data.nat.totient
data.nat.units
data.nat.with_bot
data.num.basic
data.option.basic
data.option.defs
data.option.n_ary
data.part
data.pequiv
data.pi.algebra
data.pi.lex
data.pnat.basic
data.pnat.defs
data.pnat.interval
data.polynomial.algebra_map
data.polynomial.basic
data.polynomial.cancel_leads
data.polynomial.coeff
data.polynomial.degree.definitions
data.polynomial.degree.lemmas
data.polynomial.degree.trailing_degree
data.polynomial.derivative
data.polynomial.div
data.polynomial.erase_lead
data.polynomial.eval
data.polynomial.field_division
data.polynomial.induction
data.polynomial.inductions
data.polynomial.lifts
data.polynomial.monic
data.polynomial.monomial
data.polynomial.reverse
data.polynomial.ring_division
data.polynomial.splits
data.prod.basic
data.prod.lex
data.prod.pprod
data.quot
data.rat.basic
data.rat.big_operators
data.rat.cast
data.rat.defs
data.rat.floor
data.rat.init
data.rat.lemmas
data.rat.meta_defs
data.rat.order
data.rbmap.basic
data.rbtree.default_lt
data.rbtree.init
data.real.basic
data.real.cau_seq
data.real.cau_seq_completion
data.real.ennreal
data.real.nnreal
data.real.pointwise
data.real.sqrt
data.set.Union_lift
data.set.accumulate
data.set.basic
data.set.bool_indicator
data.set.countable
data.set.finite
data.set.function
data.set.functor
data.set.image
data.set.intervals.basic
data.set.intervals.disjoint
data.set.intervals.group
data.set.intervals.infinite
data.set.intervals.instances
data.set.intervals.monoid
data.set.intervals.ord_connected
data.set.intervals.order_iso
data.set.intervals.pi
data.set.intervals.proj_Icc
data.set.intervals.unordered_interval
data.set.lattice
data.set.list
data.set.n_ary
data.set.pairwise.basic
data.set.pairwise.lattice
data.set.pointwise.basic
data.set.pointwise.big_operators
data.set.pointwise.finite
data.set.pointwise.interval
data.set.pointwise.list_of_fn
data.set.pointwise.smul
data.set.prod
data.set.semiring
data.set.sigma
data.set_like.basic
data.setoid.basic
data.sigma.basic
data.sign
data.string.defs
data.subtype
data.sum.basic
data.sum.order
data.sym.basic
data.tree
data.ulift
data.vector.basic
data.zmod.basic
data.zmod.defs
dynamics.fixed_points.basic
dynamics.periodic_pts
field_theory.finiteness
field_theory.subfield
field_theory.tower
group_theory.archimedean
group_theory.commutator
group_theory.congruence
group_theory.coset
group_theory.divisible
group_theory.finiteness
group_theory.group_action.basic
group_theory.group_action.big_operators
group_theory.group_action.conj_act
group_theory.group_action.defs
group_theory.group_action.group
group_theory.group_action.opposite
group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.quotient
group_theory.group_action.sub_mul_action
group_theory.group_action.sub_mul_action.pointwise
group_theory.group_action.units
group_theory.index
group_theory.monoid_localization
group_theory.order_of_element
group_theory.perm.basic
group_theory.perm.cycle.basic
group_theory.perm.cycle.type
group_theory.perm.fin
group_theory.perm.list
group_theory.perm.option
group_theory.perm.sign
group_theory.perm.subgroup
group_theory.perm.support
group_theory.quotient_group
group_theory.semidirect_product
group_theory.subgroup.actions
group_theory.subgroup.basic
group_theory.subgroup.finite
group_theory.subgroup.mul_opposite
group_theory.subgroup.pointwise
group_theory.subgroup.zpowers
group_theory.submonoid.basic
group_theory.submonoid.center
group_theory.submonoid.centralizer
group_theory.submonoid.membership
group_theory.submonoid.operations
group_theory.submonoid.pointwise
group_theory.subsemigroup.basic
group_theory.subsemigroup.center
group_theory.subsemigroup.centralizer
group_theory.subsemigroup.operations
linear_algebra.affine_space.affine_equiv
linear_algebra.affine_space.affine_map
linear_algebra.affine_space.affine_subspace
linear_algebra.affine_space.basic
linear_algebra.affine_space.basis
linear_algebra.affine_space.combination
linear_algebra.affine_space.independent
linear_algebra.affine_space.midpoint
linear_algebra.affine_space.midpoint_zero
linear_algebra.affine_space.restrict
linear_algebra.affine_space.slope
linear_algebra.alternating
linear_algebra.basic
linear_algebra.basis
linear_algebra.basis.bilinear
linear_algebra.bilinear_form
linear_algebra.bilinear_map
linear_algebra.determinant
linear_algebra.dfinsupp
linear_algebra.dimension
linear_algebra.direct_sum.finsupp
linear_algebra.direct_sum.tensor_product
linear_algebra.dual
linear_algebra.finite_dimensional
linear_algebra.finrank
linear_algebra.finsupp
linear_algebra.finsupp_vector_space
linear_algebra.free_module.basic
linear_algebra.free_module.finite.basic
linear_algebra.free_module.finite.matrix
linear_algebra.free_module.finite.rank
linear_algebra.free_module.rank
linear_algebra.general_linear_group
linear_algebra.invariant_basis_number
linear_algebra.isomorphisms
linear_algebra.linear_independent
linear_algebra.linear_pmap
linear_algebra.matrix.adjugate
linear_algebra.matrix.basis
linear_algebra.matrix.determinant
linear_algebra.matrix.dot_product
linear_algebra.matrix.general_linear_group
linear_algebra.matrix.mv_polynomial
linear_algebra.matrix.nonsingular_inverse
linear_algebra.matrix.polynomial
linear_algebra.matrix.reindex
linear_algebra.matrix.special_linear_group
linear_algebra.matrix.to_lin
linear_algebra.matrix.trace
linear_algebra.multilinear.basic
linear_algebra.multilinear.basis
linear_algebra.multilinear.tensor_product
linear_algebra.pi
linear_algebra.prod
linear_algebra.projection
linear_algebra.quotient
linear_algebra.ray
linear_algebra.sesquilinear_form
linear_algebra.span
linear_algebra.std_basis
linear_algebra.tensor_product
linear_algebra.tensor_product_basis
logic.basic
logic.denumerable
logic.embedding.basic
logic.embedding.set
logic.encodable.basic
logic.encodable.lattice
logic.equiv.basic
logic.equiv.defs
logic.equiv.fin
logic.equiv.fintype
logic.equiv.functor
logic.equiv.list
logic.equiv.local_equiv
logic.equiv.nat
logic.equiv.option
logic.equiv.set
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.is_empty
logic.nonempty
logic.nontrivial
logic.pairwise
logic.relation
logic.relator
logic.small.basic
logic.unique
meta.expr
meta.expr_lens
meta.rb_map
meta.univs
number_theory.divisors
number_theory.padics.padic_val
order.antichain
order.antisymmetrization
order.atoms
order.basic
order.boolean_algebra
order.bounded
order.bounded_order
order.bounds.basic
order.bounds.order_iso
order.chain
order.circular
order.closure
order.compactly_generated
order.compare
order.complete_boolean_algebra
order.complete_lattice
order.complete_lattice_intervals
order.conditionally_complete_lattice.basic
order.conditionally_complete_lattice.finset
order.conditionally_complete_lattice.group
order.copy
order.cover
order.directed
order.disjoint
order.filter.archimedean
order.filter.at_top_bot
order.filter.bases
order.filter.basic
order.filter.cofinite
order.filter.countable_Inter
order.filter.extr
order.filter.interval
order.filter.lift
order.filter.n_ary
order.filter.pi
order.filter.pointwise
order.filter.prod
order.filter.small_sets
order.filter.ultrafilter
order.fixed_points
order.galois_connection
order.heyting.basic
order.hom.basic
order.hom.bounded
order.hom.complete_lattice
order.hom.lattice
order.hom.order
order.hom.set
order.initial_seg
order.iterate
order.jordan_holder
order.lattice
order.lattice_intervals
order.liminf_limsup
order.locally_finite
order.max
order.min_max
order.minimal
order.modular_lattice
order.monotone.basic
order.monotone.odd
order.monotone.union
order.omega_complete_partial_order
order.order_iso_nat
order.partial_sups
order.prop_instances
order.rel_classes
order.rel_iso.basic
order.rel_iso.set
order.succ_pred.basic
order.succ_pred.limit
order.succ_pred.relation
order.sup_indep
order.symm_diff
order.synonym
order.upper_lower.basic
order.well_founded
order.well_founded_set
order.with_bot
order.zorn
order.zorn_atoms
ring_theory.adjoin.basic
ring_theory.algebra_tower
ring_theory.congruence
ring_theory.coprime.basic
ring_theory.coprime.lemmas
ring_theory.euclidean_domain
ring_theory.finiteness
ring_theory.ideal.basic
ring_theory.ideal.operations
ring_theory.ideal.quotient
ring_theory.ideal.quotient_operations
ring_theory.int.basic
ring_theory.localization.basic
ring_theory.localization.fraction_ring
ring_theory.multiplicity
ring_theory.mv_polynomial.symmetric
ring_theory.nilpotent
ring_theory.noetherian
ring_theory.non_zero_divisors
ring_theory.polynomial.basic
ring_theory.polynomial.content
ring_theory.polynomial.pochhammer
ring_theory.polynomial.vieta
ring_theory.principal_ideal_domain
ring_theory.simple_module
ring_theory.subring.basic
ring_theory.subsemiring.basic
ring_theory.unique_factorization_domain
ring_theory.valuation.basic
set_theory.cardinal.basic
set_theory.cardinal.cofinality
set_theory.cardinal.finite
set_theory.cardinal.ordinal
set_theory.cardinal.schroeder_bernstein
set_theory.ordinal.arithmetic
set_theory.ordinal.basic
set_theory.ordinal.exponential
set_theory.ordinal.fixed_point
set_theory.ordinal.principal
tactic.abel
tactic.algebra
tactic.alias
tactic.apply
tactic.apply_fun
tactic.assert_exists
tactic.auto_cases
tactic.binder_matching
tactic.by_contra
tactic.cache
tactic.cancel_denoms
tactic.chain
tactic.choose
tactic.clear
tactic.compute_degree
tactic.congr
tactic.congrm
tactic.converter.apply_congr
tactic.converter.interactive
tactic.converter.old_conv
tactic.core
tactic.dec_trivial
tactic.delta_instance
tactic.dependencies
tactic.derive_fintype
tactic.derive_inhabited
tactic.doc_commands
tactic.elide
tactic.explode
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.finish
tactic.generalize_proofs
tactic.generalizes
tactic.group
tactic.hint
tactic.interactive
tactic.interactive_expr
tactic.interval_cases
tactic.itauto
tactic.lean_core_docs
tactic.lift
tactic.linarith.datatypes
tactic.linarith.elimination
tactic.linarith.frontend
tactic.linarith.lemmas
tactic.linarith.parsing
tactic.linarith.preprocessing
tactic.linarith.verification
tactic.lint.basic
tactic.lint.default
tactic.lint.frontend
tactic.lint.misc
tactic.lint.simp
tactic.lint.type_classes
tactic.localized
tactic.mk_iff_of_inductive_prop
tactic.monotonicity.basic
tactic.monotonicity.interactive
tactic.nontriviality
tactic.norm_cast
tactic.norm_num
tactic.nth_rewrite.basic
tactic.nth_rewrite.congr
tactic.nth_rewrite.default
tactic.obviously
tactic.pi_instances
tactic.positivity
tactic.pretty_cases
tactic.print_sorry
tactic.project_dir
tactic.protected
tactic.push_neg
tactic.rcases
tactic.rename_var
tactic.replacer
tactic.reserved_notation
tactic.restate_axiom
tactic.rewrite
tactic.ring
tactic.ring_exp
tactic.scc
tactic.show_term
tactic.simp_command
tactic.simp_result
tactic.simp_rw
tactic.simpa
tactic.simps
tactic.solve_by_elim
tactic.split_ifs
tactic.squeeze
tactic.suggest
tactic.tauto
tactic.tfae
tactic.tidy
tactic.to_additive
tactic.transform_decl
tactic.trunc_cases
tactic.unify_equations
tactic.where
tactic.with_local_reducibility
tactic.wlog
tactic.zify
topology.G_delta
topology.algebra.affine
topology.algebra.algebra
topology.algebra.const_mul_action
topology.algebra.constructions
topology.algebra.field
topology.algebra.filter_basis
topology.algebra.group.basic
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum.basic
topology.algebra.infinite_sum.module
topology.algebra.infinite_sum.order
topology.algebra.infinite_sum.real
topology.algebra.infinite_sum.ring
topology.algebra.module.basic
topology.algebra.module.determinant
topology.algebra.module.finite_dimension
topology.algebra.module.multilinear
topology.algebra.module.simple
topology.algebra.module.star
topology.algebra.module.strong_topology
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.order.archimedean
topology.algebra.order.compact
topology.algebra.order.extend_from
topology.algebra.order.field
topology.algebra.order.group
topology.algebra.order.intermediate_value
topology.algebra.order.left_right
topology.algebra.order.liminf_limsup
topology.algebra.order.monotone_continuity
topology.algebra.order.monotone_convergence
topology.algebra.order.proj_Icc
topology.algebra.polynomial
topology.algebra.ring.basic
topology.algebra.ring.ideal
topology.algebra.star
topology.algebra.star_subalgebra
topology.algebra.uniform_convergence
topology.algebra.uniform_group
topology.algebra.uniform_mul_action
topology.algebra.uniform_ring
topology.bases
topology.basic
topology.bornology.basic
topology.bornology.constructions
topology.bornology.hom
topology.compact_open
topology.connected
topology.constructions
topology.continuous_function.basic
topology.continuous_on
topology.dense_embedding
topology.extend_from
topology.homeomorph
topology.inseparable
topology.instances.add_circle
topology.instances.ennreal
topology.instances.int
topology.instances.matrix
topology.instances.nat
topology.instances.nnreal
topology.instances.rat
topology.instances.real
topology.instances.real_vector_space
topology.instances.sign
topology.local_extr
topology.local_homeomorph
topology.locally_finite
topology.maps
topology.metric_space.algebra
topology.metric_space.antilipschitz
topology.metric_space.baire
topology.metric_space.basic
topology.metric_space.completion
topology.metric_space.emetric_space
topology.metric_space.hausdorff_distance
topology.metric_space.isometric_smul
topology.metric_space.isometry
topology.metric_space.lipschitz
topology.nhds_set
topology.noetherian_space
topology.order
topology.order.basic
topology.path_connected
topology.quasi_separated
topology.separation
topology.sequences
topology.sets.closeds
topology.sets.compacts
topology.sets.opens
topology.subset_properties
topology.support
topology.tactic
topology.uniform_space.abstract_completion
topology.uniform_space.basic
topology.uniform_space.cauchy
topology.uniform_space.compact
topology.uniform_space.complete_separated
topology.uniform_space.completion
topology.uniform_space.equicontinuity
topology.uniform_space.equiv
topology.uniform_space.pi
topology.uniform_space.separation
topology.uniform_space.uniform_convergence
topology.uniform_space.uniform_convergence_topology
topology.uniform_space.uniform_embedding
topology.unit_interval

debugger.attr

source

meta def debugger.attr :

(user_attribute unit)

General documentation

Library

LeanChemicalTheories

adsorption

BETInfinite

langmuir_kinetics

dimensional_analysis

basic

buckingham_pi

math

antideriv

deriv

infinite_series

rpow

molecular_mechanics

lennard_jones

translation_invariance_LJ

physics

kinematic_equations

thermodynamics

basic

boyles_law

core

data

buffer

dlist

vector

init

algebra

classes

functions

order

control

alternative

applicative

combinators

except

functor

id

lawful

lift

monad

monad_fail

option

reader

state

data

array

basic

slice

bool

basic

lemmas

char

basic

classes

lemmas

fin

basic

ops

int

basic

bitwise

comp_lemmas

order

list

basic

instances

lemmas

qsort

nat

basic

bitwise

div

gcd

lemmas

option

basic

instances

ordering

basic

lemmas

sigma

basic

lex

string

basic

ops

subtype

basic

instances

sum

basic

unsigned

basic

ops

prod

punit

quot

repr

set

setoid

to_string

mathlib

algebra

subalgebra

basic

tower

basic

bilinear

equiv

hom

operations

pi

prod

restrict_scalars

tower

big_operators

multiset

basic

lemmas

associated

basic

fin

finprod

finsupp

intervals

nat_antidiagonal

option

order

pi

ring

ring_equiv

char_p

basic

invertible

two

char_zero

defs

infinite

lemmas

quotient

direct_sum

basic

finsupp

module

divisibility

basic

units

euclidean_domain

basic

defs

instances

field

basic

defs

opposite

free_monoid

basic

gcd_monoid

basic

finset

multiset

group

with_one

defs

basic

commutator

commute

conj

defs

inj_surj

opposite

order_synonym

pi

prod

semiconj

type_tags

ulift

units

group_power

basic

lemmas

order

ring

group_ring_action

basic

subobjects

group_with_zero

units

basic

lemmas

basic

commute

defs

divisibility

inj_surj

power

semiconj

hom

equiv

units

basic

group_with_zero

basic

aut

commute

embedding

group

group_action

group_instances

iterate

non_unital_alg

ring

units

module

submodule

basic

bilinear

lattice

pointwise

algebra

basic

big_operators

equiv

hom

linear_map

opposites

pi

prod

ulift

monoid_algebra

basic

division

support

order

field

canonical

basic

defs

basic

defs

inj_surj

power

group

abs

bounds

defs

inj_surj

instances

min_max

order_iso

type_tags

units

hom

basic

monoid

cancel

basic

defs

canonical

defs

with_zero

basic

defs

basic

defs

lemmas

min_max

nat_cast

order_dual

prod

type_tags

units

with_top

nonneg

field

floor

ring

positive

ring

abs

canonical

char_zero

defs

inj_surj

lemmas

with_top

sub

canonical

defs

with_top

absolute_value

archimedean

floor

invertible

kleene

module

pi

smul

to_interval_mod

with_zero

zero_le_one

polynomial

big_operators

regular

basic

smul

ring

add_aut

aut

basic

commute

comp_typeclasses

defs

divisibility

equiv

fin

idempotents

inj_surj

opposite

pi

prod

regular

semiconj

ulift

units

star

basic

big_operators

module

order

pi

pointwise

prod

self_adjoint

star_alg_hom

subalgebra

unitary

abs

add_torsor

associated

bounds

covariant_and_contravariant

geom_sum

indicator_function

invertible

modeq

ne_zero

opposites

parity

periodic

punit_instances

quotient

smul_with_zero

support

analysis

asymptotics

asymptotic_equivalent

asymptotics

theta

calculus

conformal

normed_space

deriv

add

basic

comp

inv

inverse

linear

mul

polynomial

pow

prod

slope

zpow

fderiv

add

basic

bilinear

comp

equiv

linear

mul

prod

restrict_scalars

cont_diff

cont_diff_def

extend_deriv

formal_multilinear_series

inverse

iterated_deriv

lhopital

local_extr

mean_value

tangent_cone

complex

basic

circle

conformal

isometry

real_deriv

convex

basic

combination

function

hull

jensen

normed

segment

slope

star

strict

strict_convex_space

topology

uniform

inner_product_space

basic

locally_convex

balanced_core_hull

basic

bounded

normed

field

basic

unit_ball

group

add_circle

add_torsor

ball_sphere

basic

completion

hom

infinite_sum

pointwise

quotient

seminorm

order

basic

mul_action

normed_space

star

basic

add_torsor

affine_isometry

banach

basic

bounded_linear_maps

completion

conformal_linear_map

continuous_linear_map

finite_dimension

linear_isometry

multilinear

operator_norm

pointwise

ray

riesz_lemma

units

special_functions

complex

arg

log

log_deriv

log

basic

deriv

pow

asymptotics

complex

continuity

deriv

nnreal

real

trigonometric

angle

basic

deriv

inverse

exp

exp_deriv

specific_limits

basic

normed

seminorm

combinatorics

composition

partition

control

monad

basic

traversable

basic

derive

instances

lemmas

applicative

basic

bifunctor

equiv_functor

functor

data

bool

basic

set

complex

basic

exponential

module

countable

basic

defs

dfinsupp

basic

dlist

basic

enat

basic

lattice

fin

tuple

basic

interval

vec_notation

finite

basic

card

defs

set

finset

basic

card

fin

fold

image

lattice

locally_finite

n_ary

nat_antidiagonal

noncomm_prod

option

order

pairwise

pi

pointwise

powerset

preimage

prod

sigma

sort

sum

finsupp

antidiagonal

basic

defs

fin

indicator

multiset

order

to_dfinsupp

fintype

basic

big_operators

card

fin

lattice

list

option

perm

pi

powerset

prod

sigma

sort

sum

units

vector

fun_like

basic

embedding

equiv

int

cast

basic

defs

field

lemmas

prod

dvd

basic

order

basic

lemmas

units

basic

bitwise

char_zero

div

gcd

interval

least_greatest

lemmas

modeq

parity

succ_pred

units

is_R_or_C

basic

list

big_operators

basic

lemmas

basic

chain

count

cycle

dedup

defs

duplicate

fin_range

forall2

infix

join

lattice

lex

min_max

nat_antidiagonal

nodup

nodup_equiv_fin

of_fn

pairwise

perm

permutation

prime

prod_sigma

range

rotate

sort

sublists

tfae

zip

matrix

basic

basis

block

notation

pequiv

rank

multiset

antidiagonal

basic

bind

dedup

finset_ops

fold

lattice

nat_antidiagonal

nodup

pi

powerset

range

sort

sum

mv_polynomial

basic

comm_ring

equiv

rename

variables

nat

cast

basic

defs

field

prod

choose

basic

cast

sum

factorial

basic

cast

factorization

basic

gcd

basic

order

basic

lemmas

basic

bits

bitwise

count

factors

interval

lattice

log

modeq

multiplicity

pairing

parity

part_enat

periodic

pow

prime

prime_fin

set

size

sqrt

succ_pred

totient

units

with_bot

num

basic

option

basic

defs

n_ary

pi

algebra

lex

pnat

basic

defs

interval

polynomial

degree

definitions

lemmas

trailing_degree

algebra_map

basic

cancel_leads

coeff

derivative

div

erase_lead

eval

field_division

induction

inductions

lifts

monic

monomial

reverse

ring_division

splits

prod

basic

lex

pprod

rat

basic

big_operators

cast

defs

floor

init

lemmas

meta_defs

order

rbmap

basic

rbtree

default_lt

init

real

basic

cau_seq

cau_seq_completion

ennreal

nnreal

pointwise

sqrt

set

intervals

basic

disjoint

group

infinite

instances

monoid

ord_connected

order_iso

pi

proj_Icc

unordered_interval

pairwise

basic

lattice

pointwise

basic

big_operators

finite

interval

list_of_fn

smul

Union_lift

accumulate

basic

bool_indicator

countable

finite

function

functor

image

lattice

list

n_ary

prod

semiring

sigma

set_like

basic

setoid

basic

sigma

basic

string

defs

sum

basic

order

sym

basic

vector

basic

zmod

basic

defs

bracket

fin_enum

mllist

part

pequiv

quot

sign

subtype

tree

ulift

dynamics

fixed_points

basic

periodic_pts

field_theory

finiteness

subfield

tower

group_theory

group_action

sub_mul_action

pointwise

basic

big_operators

conj_act

defs

group

opposite

pi

prod

quotient

sub_mul_action

units

perm

cycle

basic

type

basic

fin

list

option

sign

subgroup

support

subgroup

actions

basic

finite

mul_opposite

pointwise

zpowers

submonoid

basic

center

centralizer

membership

operations

pointwise

subsemigroup

basic

center

centralizer

operations

archimedean

commutator

congruence

coset

divisible

finiteness

index

monoid_localization

order_of_element

quotient_group

semidirect_product

linear_algebra

affine_space

affine_equiv

affine_map

affine_subspace

basic

basis

combination

independent

midpoint

midpoint_zero

restrict

slope

basis

bilinear

direct_sum

finsupp

tensor_product

free_module

finite

basic

matrix

rank

basic

rank

matrix

adjugate

basis

determinant

dot_product

general_linear_group

mv_polynomial

nonsingular_inverse

polynomial

reindex

special_linear_group

to_lin

trace

multilinear

basic

basis

tensor_product

alternating

basic

basis

bilinear_form

bilinear_map

determinant

dfinsupp

dimension

dual

finite_dimensional

finrank

finsupp

finsupp_vector_space

general_linear_group

invariant_basis_number

isomorphisms

linear_independent

linear_pmap

pi

prod

projection

quotient

ray

sesquilinear_form

span

std_basis

tensor_product

tensor_product_basis

logic

embedding

basic

set

encodable

basic

lattice

equiv

basic

defs

fin

fintype

functor

list

local_equiv

nat

option

set

function

basic

conjugate

iterate

small

basic

denumerable

is_empty

nonempty

nontrivial

pairwise

relation

relator

unique

Additional documentation

Color scheme

dark system light