mathlib3
documentation
core
/
init
.
default
Google site search
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
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.spectrum
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.decomposition
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.cont_diff
analysis.calculus.cont_diff_def
analysis.calculus.deriv.add
analysis.calculus.deriv.basic
analysis.calculus.deriv.comp
analysis.calculus.deriv.inverse
analysis.calculus.deriv.mul
analysis.calculus.deriv.polynomial
analysis.calculus.deriv.pow
analysis.calculus.deriv.slope
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.lagrange_multipliers
analysis.calculus.local_extr
analysis.calculus.mean_value
analysis.calculus.tangent_cone
analysis.complex.basic
analysis.convex.basic
analysis.convex.combination
analysis.convex.cone.basic
analysis.convex.function
analysis.convex.hull
analysis.convex.jensen
analysis.convex.normed
analysis.convex.segment
analysis.convex.slope
analysis.convex.specific_functions.basic
analysis.convex.star
analysis.convex.strict
analysis.convex.strict_convex_space
analysis.convex.topology
analysis.convex.uniform
analysis.inner_product_space.adjoint
analysis.inner_product_space.basic
analysis.inner_product_space.calculus
analysis.inner_product_space.dual
analysis.inner_product_space.orthogonal
analysis.inner_product_space.pi_L2
analysis.inner_product_space.positive
analysis.inner_product_space.projection
analysis.inner_product_space.rayleigh
analysis.inner_product_space.spectrum
analysis.inner_product_space.symmetric
analysis.locally_convex.balanced_core_hull
analysis.locally_convex.basic
analysis.locally_convex.bounded
analysis.locally_convex.polar
analysis.mean_inequalities
analysis.normed.field.basic
analysis.normed.group.add_circle
analysis.normed.group.add_torsor
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.continuous_linear_map
analysis.normed_space.dual
analysis.normed_space.extend
analysis.normed_space.finite_dimension
analysis.normed_space.hahn_banach.extension
analysis.normed_space.is_R_or_C
analysis.normed_space.linear_isometry
analysis.normed_space.multilinear
analysis.normed_space.operator_norm
analysis.normed_space.pi_Lp
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.exp
analysis.special_functions.log.basic
analysis.special_functions.pow.complex
analysis.special_functions.pow.nnreal
analysis.special_functions.pow.real
analysis.special_functions.sqrt
analysis.special_functions.trigonometric.angle
analysis.special_functions.trigonometric.basic
analysis.special_functions.trigonometric.inverse
analysis.specific_limits.basic
analysis.specific_limits.normed
analysis.von_neumann_algebra.basic
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.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.order
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.is_R_or_C.lemmas
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.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.dmatrix
data.matrix.invertible
data.matrix.kronecker
data.matrix.notation
data.matrix.pequiv
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.expand
data.polynomial.field_division
data.polynomial.induction
data.polynomial.inductions
data.polynomial.integral_normalization
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.conjugate_exponents
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.sigma.lex
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.minpoly.basic
field_theory.minpoly.field
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.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.charpoly.basic
linear_algebra.contraction
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.eigenspace.basic
linear_algebra.eigenspace.minpoly
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.free_module.strong_rank_condition
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.bilinear_form
linear_algebra.matrix.block
linear_algebra.matrix.charpoly.basic
linear_algebra.matrix.charpoly.coeff
linear_algebra.matrix.charpoly.linear_map
linear_algebra.matrix.determinant
linear_algebra.matrix.general_linear_group
linear_algebra.matrix.hermitian
linear_algebra.matrix.mv_polynomial
linear_algebra.matrix.nondegenerate
linear_algebra.matrix.nonsingular_inverse
linear_algebra.matrix.polynomial
linear_algebra.matrix.pos_def
linear_algebra.matrix.reindex
linear_algebra.matrix.sesquilinear_form
linear_algebra.matrix.special_linear_group
linear_algebra.matrix.spectrum
linear_algebra.matrix.symmetric
linear_algebra.matrix.to_lin
linear_algebra.matrix.to_linear_equiv
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.projective_space.basic
linear_algebra.quadratic_form.basic
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
linear_algebra.trace
linear_algebra.unitary_group
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.equiv.transfer_instance
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.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.adjoin.fg
ring_theory.adjoin.tower
ring_theory.algebra_tower
ring_theory.algebraic
ring_theory.congruence
ring_theory.coprime.basic
ring_theory.coprime.lemmas
ring_theory.euclidean_domain
ring_theory.finite_type
ring_theory.finiteness
ring_theory.ideal.basic
ring_theory.ideal.local_ring
ring_theory.ideal.operations
ring_theory.ideal.quotient
ring_theory.ideal.quotient_operations
ring_theory.int.basic
ring_theory.integral_closure
ring_theory.jacobson_ideal
ring_theory.localization.basic
ring_theory.localization.fraction_ring
ring_theory.localization.integer
ring_theory.matrix_algebra
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.quotient
ring_theory.polynomial.scale_roots
ring_theory.polynomial.tower
ring_theory.polynomial.vieta
ring_theory.polynomial_algebra
ring_theory.principal_ideal_domain
ring_theory.simple_module
ring_theory.subring.basic
ring_theory.subsemiring.basic
ring_theory.tensor_product
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.linear_combination
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.mk_simp_attribute
tactic.monotonicity.basic
tactic.monotonicity.interactive
tactic.noncomm_ring
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.module.weak_dual
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
linear_algebra.End
linear_algebra.blackbox
linear_algebra.direct_sum_from_to
linear_algebra.inner_aut
linear_algebra.invariant_submodule
linear_algebra.is_proj'
linear_algebra.is_real
linear_algebra.kronecker_to_tensor
linear_algebra.lmul_rmul
linear_algebra.mul''
linear_algebra.my_bimodule
linear_algebra.my_ips.basic
linear_algebra.my_ips.frob
linear_algebra.my_ips.functional
linear_algebra.my_ips.ips
linear_algebra.my_ips.mat_ips
linear_algebra.my_ips.minimal_proj
linear_algebra.my_ips.mul_op
linear_algebra.my_ips.nontracial
linear_algebra.my_ips.op_unop
linear_algebra.my_ips.pos
linear_algebra.my_ips.quantum_set
linear_algebra.my_ips.rank_one
linear_algebra.my_ips.strict
linear_algebra.my_ips.symm
linear_algebra.my_ips.tensor_hilbert
linear_algebra.my_ips.vn
linear_algebra.my_matrix.basic
linear_algebra.my_matrix.conj
linear_algebra.my_matrix.include_block
linear_algebra.my_matrix.is_almost_hermitian
linear_algebra.my_matrix.pos_def_rpow
linear_algebra.my_matrix.pos_eq_linear_map_is_positive
linear_algebra.my_matrix.reshape
linear_algebra.my_matrix.spectra
linear_algebra.my_matrix.star_ordered_ring
linear_algebra.my_spec
linear_algebra.my_tensor_product
linear_algebra.nacgor
linear_algebra.of_norm
linear_algebra.pi_direct_sum
linear_algebra.pi_star_ordered_ring
linear_algebra.tensor_finite
linear_algebra.to_matrix_of_equiv
other.sonia
preq.complex
preq.dite
preq.equiv
preq.finset
preq.is_R_or_C_le
preq.ites
preq.star_alg_equiv
quantum_graph.example
quantum_graph.iso
quantum_graph.mess
quantum_graph.nontracial
quantum_graph.qam_A
quantum_graph.qam_A_example
quantum_graph.schur_idempotent
quantum_graph.symm
quantum_graph.to_projections
rep_theory.aut_mat
debugger
.
attr
source
meta
def
debugger
.
attr
:
(
user_attribute
unit
)
General documentation
index
foundational types
tactics
commands
hole commands
attributes
notes
references
Additional documentation
Library
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
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
feature_search
float
format
fun_info
has_reflect
hole_command
injection_tactic
instance_cache
interaction_monad
interactive
interactive_base
json
level
local_context
match_tactic
mk_dec_eq_instance
mk_has_reflect_instance
mk_has_sizeof_instance
mk_inhabited_instance
module_info
name
occurrences
options
pexpr
rb_map
rec_util
ref
relation_tactics
rewrite_tactic
set_get_option_tactics
simp_tactic
tactic
tagged_format
task
type_context
vm
well_founded_tactics
cc_lemmas
classical
coe
core
default
function
funext
ite_simp
logic
propext
util
version
wf
system
io
io_interface
random
mathlib
algebra
algebra
subalgebra
basic
tower
basic
bilinear
equiv
hom
operations
pi
prod
restrict_scalars
spectrum
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
decomposition
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
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
deriv
add
basic
comp
inverse
mul
polynomial
pow
slope
fderiv
add
basic
bilinear
comp
equiv
linear
mul
prod
restrict_scalars
cont_diff
cont_diff_def
formal_multilinear_series
inverse
lagrange_multipliers
local_extr
mean_value
tangent_cone
complex
basic
convex
cone
basic
specific_functions
basic
basic
combination
function
hull
jensen
normed
segment
slope
star
strict
strict_convex_space
topology
uniform
inner_product_space
adjoint
basic
calculus
dual
orthogonal
pi_L2
positive
projection
rayleigh
spectrum
symmetric
locally_convex
balanced_core_hull
basic
bounded
polar
normed
field
basic
group
add_circle
add_torsor
basic
completion
hom
infinite_sum
pointwise
quotient
seminorm
order
basic
mul_action
normed_space
hahn_banach
extension
star
basic
add_torsor
affine_isometry
banach
basic
bounded_linear_maps
completion
continuous_linear_map
dual
extend
finite_dimension
is_R_or_C
linear_isometry
multilinear
operator_norm
pi_Lp
pointwise
ray
riesz_lemma
units
special_functions
complex
arg
log
log
basic
pow
complex
nnreal
real
trigonometric
angle
basic
inverse
exp
sqrt
specific_limits
basic
normed
von_neumann_algebra
basic
mean_inequalities
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
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
order
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
lemmas
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
range
rotate
sort
sublists
tfae
zip
matrix
basic
basis
block
dmatrix
invertible
kronecker
notation
pequiv
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
expand
field_division
induction
inductions
integral_normalization
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
conjugate_exponents
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
lex
string
defs
sum
basic
order
sym
basic
vector
basic
zmod
basic
defs
bracket
mllist
part
pequiv
quot
sign
subtype
tree
ulift
dynamics
fixed_points
basic
periodic_pts
field_theory
minpoly
basic
field
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
linear_algebra
affine_space
affine_equiv
affine_map
affine_subspace
basic
basis
combination
independent
midpoint
midpoint_zero
restrict
slope
basis
bilinear
charpoly
basic
direct_sum
finsupp
tensor_product
eigenspace
basic
minpoly
free_module
finite
basic
matrix
rank
basic
rank
strong_rank_condition
matrix
charpoly
basic
coeff
linear_map
adjugate
basis
bilinear_form
block
determinant
general_linear_group
hermitian
mv_polynomial
nondegenerate
nonsingular_inverse
polynomial
pos_def
reindex
sesquilinear_form
special_linear_group
spectrum
symmetric
to_lin
to_linear_equiv
trace
multilinear
basic
basis
tensor_product
projective_space
basic
quadratic_form
basic
alternating
basic
basis
bilinear_form
bilinear_map
contraction
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
trace
unitary_group
logic
embedding
basic
set
encodable
basic
lattice
equiv
basic
defs
fin
fintype
functor
list
local_equiv
nat
option
set
transfer_instance
function
basic
conjugate
iterate
small
basic
basic
denumerable
is_empty
nonempty
nontrivial
pairwise
relation
relator
unique
meta
expr
expr_lens
rb_map
univs
number_theory
padics
padic_val
divisors
order
bounds
basic
order_iso
conditionally_complete_lattice
basic
finset
group
filter
archimedean
at_top_bot
bases
basic
cofinite
countable_Inter
extr
interval
lift
n_ary
pi
pointwise
prod
small_sets
ultrafilter
heyting
basic
hom
basic
bounded
complete_lattice
lattice
order
set
monotone
basic
rel_iso
basic
set
succ_pred
basic
limit
relation
upper_lower
basic
antichain
antisymmetrization
atoms
basic
boolean_algebra
bounded
bounded_order
chain
circular
closure
compactly_generated
compare
complete_boolean_algebra
complete_lattice
complete_lattice_intervals
copy
cover
directed
disjoint
fixed_points
galois_connection
initial_seg
iterate
jordan_holder
lattice
lattice_intervals
liminf_limsup
locally_finite
max
min_max
minimal
modular_lattice
omega_complete_partial_order
order_iso_nat
partial_sups
prop_instances
rel_classes
sup_indep
symm_diff
synonym
well_founded
well_founded_set
with_bot
zorn
zorn_atoms
ring_theory
adjoin
basic
fg
tower
coprime
basic
lemmas
ideal
basic
local_ring
operations
quotient
quotient_operations
int
basic
localization
basic
fraction_ring
integer
mv_polynomial
symmetric
polynomial
basic
content
pochhammer
quotient
scale_roots
tower
vieta
subring
basic
subsemiring
basic
valuation
basic
algebra_tower
algebraic
congruence
euclidean_domain
finite_type
finiteness
integral_closure
jacobson_ideal
matrix_algebra
multiplicity
nilpotent
noetherian
non_zero_divisors
polynomial_algebra
principal_ideal_domain
simple_module
tensor_product
unique_factorization_domain
set_theory
cardinal
basic
cofinality
finite
ordinal
schroeder_bernstein
ordinal
arithmetic
basic
exponential
fixed_point
principal
tactic
converter
apply_congr
interactive
old_conv
linarith
datatypes
elimination
frontend
lemmas
parsing
preprocessing
verification
lint
basic
default
frontend
misc
simp
type_classes
monotonicity
basic
interactive
nth_rewrite
basic
congr
default
abel
algebra
alias
apply
apply_fun
assert_exists
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
compute_degree
congr
congrm
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elide
explode
ext
field_simp
fin_cases
find
finish
generalize_proofs
generalizes
group
hint
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
linear_combination
localized
mk_iff_of_inductive_prop
mk_simp_attribute
noncomm_ring
nontriviality
norm_cast
norm_num
obviously
pi_instances
positivity
pretty_cases
print_sorry
project_dir
protected
push_neg
rcases
rename_var
replacer
reserved_notation
restate_axiom
rewrite
ring
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
solve_by_elim
split_ifs
squeeze
suggest
tauto
tfae
tidy
to_additive
transform_decl
trunc_cases
unify_equations
where
with_local_reducibility
wlog
zify
topology
algebra
group
basic
infinite_sum
basic
module
order
real
ring
module
basic
determinant
finite_dimension
multilinear
simple
star
strong_topology
weak_dual
order
archimedean
compact
extend_from
field
group
intermediate_value
left_right
liminf_limsup
monotone_continuity
monotone_convergence
proj_Icc
ring
basic
ideal
affine
algebra
const_mul_action
constructions
field
filter_basis
group_completion
group_with_zero
monoid
mul_action
polynomial
star
star_subalgebra
uniform_convergence
uniform_group
uniform_mul_action
uniform_ring
bornology
basic
constructions
hom
continuous_function
basic
instances
add_circle
ennreal
int
matrix
nat
nnreal
rat
real
real_vector_space
sign
metric_space
algebra
antilipschitz
baire
basic
completion
emetric_space
hausdorff_distance
isometric_smul
isometry
lipschitz
order
basic
sets
closeds
compacts
opens
uniform_space
abstract_completion
basic
cauchy
compact
complete_separated
completion
equicontinuity
equiv
pi
separation
uniform_convergence
uniform_convergence_topology
uniform_embedding
G_delta
bases
basic
compact_open
connected
constructions
continuous_on
dense_embedding
extend_from
homeomorph
inseparable
local_extr
local_homeomorph
locally_finite
maps
nhds_set
noetherian_space
order
path_connected
quasi_separated
separation
sequences
subset_properties
support
tactic
unit_interval
monlib
linear_algebra
my_ips
basic
frob
functional
ips
mat_ips
minimal_proj
mul_op
nontracial
op_unop
pos
quantum_set
rank_one
strict
symm
tensor_hilbert
vn
my_matrix
basic
conj
include_block
is_almost_hermitian
pos_def_rpow
pos_eq_linear_map_is_positive
reshape
spectra
star_ordered_ring
End
blackbox
direct_sum_from_to
inner_aut
invariant_submodule
is_proj'
is_real
kronecker_to_tensor
lmul_rmul
mul''
my_bimodule
my_spec
my_tensor_product
nacgor
of_norm
pi_direct_sum
pi_star_ordered_ring
tensor_finite
to_matrix_of_equiv
other
sonia
preq
complex
dite
equiv
finset
is_R_or_C_le
ites
star_alg_equiv
quantum_graph
example
iso
mess
nontracial
qam_A
qam_A_example
schur_idempotent
symm
to_projections
rep_theory
aut_mat
Color scheme
dark
system
light