DirichletTheorem

📁 Source: Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Statistics

Metric	Count
Definitions basisModTorsion, basisUnitLattice, logSpace, seq, w₀, fundSystem, logEmbedding, logEmbeddingEquiv, logEmbeddingQuot, rank, unitLattice	11
Theorems closure_fundSystem_sup_torsion_eq_top, exists_unit, logEmbedding_component, logEmbedding_component_le, logEmbedding_eq_zero_iff, logEmbedding_ker, log_le_of_logEmbedding_le, map_logEmbedding_sup_torsion, mult_log_place_eq_zero, seq_decreasing, seq_ne_zero, seq_next, seq_norm_le, sum_logEmbedding_component, unitLattice_inter_ball_finite, unitLattice_span_eq_top, exist_unique_eq_mul_prod, finrank_eq_rank, fun_eq_repr, fundSystem_mk, instDiscrete_unitLattice, instFGUnitsRingOfIntegers, instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, instFiniteIntAdditiveUnitsRingOfIntegers, instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, instZLattice_unitLattice, logEmbeddingEquiv_apply, logEmbeddingQuot_apply, logEmbeddingQuot_injective, logEmbedding_fundSystem, rank_modTorsion, unitLattice_rank	32
Total	43

NumberField.Units

Definitions

Name	Category	Theorems
basisModTorsion 📖	CompOp	2 math math: fun_eq_repr, fundSystem_mk
basisUnitLattice 📖	CompOp	5 math math: logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, basisOfIsMaxRank_fundSystem, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
fundSystem 📖	CompOp	13 math math: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, isMaxRank_fundSystem, regulator_eq_det, fundSystem_mk, closure_fundSystem_sup_torsion_eq_top, regulator_eq_regOfFamily_fundSystem, exist_unique_eq_mul_prod, finrank_mul_regulator_eq_det, regulator_eq_det', basisOfIsMaxRank_fundSystem, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne
logEmbedding 📖	CompOp	14 math math: logEmbedding_fundSystem, span_basisOfIsMaxRank, logEmbeddingQuot_apply, basisOfIsMaxRank_apply, dirichletUnitTheorem.map_logEmbedding_sup_torsion, dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.logMap_eq_logEmbedding, dirichletUnitTheorem.logEmbedding_eq_zero_iff, NumberField.mixedEmbedding.logMap_unit_smul, dirichletUnitTheorem.logEmbedding_component, logEmbeddingEquiv_apply, regulator_eq_det', dirichletUnitTheorem.logEmbedding_ker, regOfFamily_eq_det'
logEmbeddingEquiv 📖	CompOp	1 math math: logEmbeddingEquiv_apply
logEmbeddingQuot 📖	CompOp	2 math math: logEmbeddingQuot_apply, logEmbeddingQuot_injective
rank 📖	CompOp	30 math math: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', finrank_eq_rank, logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, NumberField.IsCMField.units_rank_eq_units_rank, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, regOfFamily_eq_det, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv, span_basisOfIsMaxRank, basisOfIsMaxRank_apply, regulator_eq_det, finrank_mul_regOfFamily_eq_det, fundSystem_mk, rank_modTorsion, regOfFamily_of_isMaxRank, regOfFamily_div_regulator, NumberField.IsCMField.closure_realFundSystem_sup_torsion, closure_fundSystem_sup_torsion_eq_top, abs_det_eq_abs_det, unitLattice_rank, isMaxRank_iff_closure_finiteIndex, exist_unique_eq_mul_prod, finrank_mul_regulator_eq_det, regulator_eq_det', basisOfIsMaxRank_fundSystem, regOfFamily_eq_det', NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.IsCMField.regOfFamily_realFunSystem, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
unitLattice 📖	CompOp	11 math math: logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, instZLattice_unitLattice, dirichletUnitTheorem.unitLattice_span_eq_top, dirichletUnitTheorem.unitLattice_inter_ball_finite, instDiscrete_unitLattice, unitLattice_rank, logEmbeddingEquiv_apply, basisOfIsMaxRank_fundSystem, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_fundSystem_sup_torsion_eq_top 📖	mathematical	—	Subgroup Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.closure Set.range rank fundSystem torsion Top.top Subgroup.instTop	—	Subgroup.eq_top_iff' sup_comm exist_unique_eq_mul_prod Subgroup.mul_mem_sup SetLike.coe_mem Subgroup.prod_mem Subgroup.zpow_mem Subgroup.subset_closure Set.mem_range_self
exist_unique_eq_mul_prod 📖	mathematical	—	ExistsUnique Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike torsion Units.instMul Finset.prod rank CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid Finset.univ Fin.fintype DivInvMonoid.toZPow Units.instDivInvMonoid fundSystem	—	RingHomInvPair.ids Subgroup.normal_of_comm QuotientGroup.eq_one_iff QuotientGroup.mk_mul QuotientGroup.mk_inv ofMul_eq_zero ofMul_mul ofMul_inv QuotientGroup.mk_prod ofMul_prod Finset.sum_congr QuotientGroup.out_eq' add_eq_zero_iff_eq_neg neg_neg Module.Basis.sum_repr Finset.prod_congr inv_mul_cancel_right fun_eq_repr mul_inv_cancel_right
finrank_eq_rank 📖	mathematical	—	Module.finrank Real dirichletUnitTheorem.logSpace Real.semiring Pi.addCommMonoid NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal rank	—	Module.finrank_fintype_fun_eq_card commRing_strongRankCondition Real.instNontrivial Fintype.card_subtype_compl
fun_eq_repr 📖	mathematical	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike torsion Units.instMul Finset.prod rank CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid Finset.univ Fin.fintype DivInvMonoid.toZPow Units.instDivInvMonoid fundSystem	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Int.instSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Additive HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup Additive.addCommMonoid QuotientGroup.Quotient.commGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toIntModule Additive.addCommGroup Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisModTorsion Equiv Equiv.instEquivLike Additive.ofMul	—	Subgroup.normal_of_comm QuotientGroup.mk_mul QuotientGroup.eq_one_iff one_mul QuotientGroup.mk_prod ofMul_prod Finset.sum_congr QuotientGroup.out_eq' RingHomInvPair.ids Module.Basis.repr_sum_self
fundSystem_mk 📖	mathematical	—	DFunLike.coe Equiv HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul fundSystem Module.Basis rank Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid QuotientGroup.Quotient.commGroup Units.instCommGroupUnits CommRing.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup Module.Basis.instFunLike basisModTorsion	—	Quotient.out_eq'
instDiscrete_unitLattice 📖	mathematical	—	DiscreteTopology dirichletUnitTheorem.logSpace Submodule Int.instSemiring Pi.addCommMonoid NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike unitLattice instTopologicalSpaceSubtype Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	discreteTopology_of_isOpen_singleton_zero IsTopologicalAddGroup.toContinuousAdd Submodule.topologicalAddGroup Pi.topologicalAddGroup instIsTopologicalAddGroupReal isOpen_singleton_of_finite_mem_nhds Subtype.t1Space instT1SpaceForall T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Metric.closedBall_mem_nhds Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.Finite.of_finite_image Set.ext Subtype.mem dirichletUnitTheorem.unitLattice_inter_ball_finite Set.injOn_of_injective Subtype.val_injective
instFGUnitsRingOfIntegers 📖	mathematical	—	Monoid.FG Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instMonoid	—	Monoid.fg_iff_add_fg AddGroup.fg_iff_addMonoid_fg Module.Finite.iff_addGroup_fg instFiniteIntAdditiveUnitsRingOfIntegers
instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion 📖	mathematical	—	Module.Finite Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid QuotientGroup.Quotient.commGroup Units.instCommGroupUnits CommRing.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup	—	Module.Finite.equiv instModuleFinite_of_discrete_submodule FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real instDiscrete_unitLattice RingHomInvPair.ids
instFiniteIntAdditiveUnitsRingOfIntegers 📖	mathematical	—	Module.Finite Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup	—	Module.finite_def Submodule.fg_of_fg_map_of_fg_inf_ker Subgroup.normal_of_comm RingHomSurjective.ids Submodule.map_top LinearMap.range_eq_top QuotientGroup.mk'_surjective instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion inf_of_le_right le_top AddMonoidHom.coe_toIntLinearMap_ker MonoidHom.coe_toAdditive_ker QuotientGroup.ker_mk' Submodule.fg_iff_addSubgroup_fg AddSubgroup.toIntSubmodule_toAddSubgroup AddGroup.fg_iff_addSubgroup_fg Finite.of_fintype AddGroup.fg_of_finite
instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion 📖	mathematical	—	Module.Free Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid QuotientGroup.Quotient.commGroup Units.instCommGroupUnits CommRing.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup	—	Module.Free.of_equiv instModuleFree_of_discrete_submodule FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real instDiscrete_unitLattice RingHomInvPair.ids
instZLattice_unitLattice 📖	mathematical	—	IsZLattice Real Real.normedField dirichletUnitTheorem.logSpace Pi.normedAddCommGroup NumberField.InfinitePlace dirichletUnitTheorem.w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal unitLattice instDiscrete_unitLattice	—	instDiscrete_unitLattice dirichletUnitTheorem.unitLattice_span_eq_top
logEmbeddingEquiv_apply 📖	mathematical	—	dirichletUnitTheorem.logSpace Submodule Int.instSemiring Pi.addCommMonoid NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike unitLattice DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion Additive.addCommMonoid CommGroup.toCommMonoid QuotientGroup.Quotient.commGroup Units.instCommGroupUnits CommRing.toCommMonoid Submodule.addCommMonoid Additive.addCommGroup Submodule.addCommGroup Int.instRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv logEmbeddingEquiv Equiv Equiv.instEquivLike Additive.ofMul AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbedding	—	RingHomInvPair.ids
logEmbeddingQuot_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion dirichletUnitTheorem.logSpace AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group Subgroup.normal_of_comm Units.instCommGroupUnits CommRing.toCommMonoid Pi.addZeroClass NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbeddingQuot Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Units.instMulOneClass logEmbedding	—	Subgroup.normal_of_comm
logEmbeddingQuot_injective 📖	mathematical	—	Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion dirichletUnitTheorem.logSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group Subgroup.normal_of_comm Units.instCommGroupUnits CommRing.toCommMonoid Pi.addZeroClass NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbeddingQuot	—	Subgroup.normal_of_comm EmbeddingLike.apply_eq_iff_eq EquivLike.toEmbeddingLike MonoidHom.normal_ker QuotientGroup.kerLift_injective
logEmbedding_fundSystem 📖	mathematical	—	DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing dirichletUnitTheorem.logSpace AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul fundSystem Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike unitLattice Module.Basis rank Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike basisUnitLattice	—	basisUnitLattice.eq_1 RingHomInvPair.ids Module.Basis.map_apply logEmbeddingEquiv_apply
rank_modTorsion 📖	mathematical	—	Module.finrank Additive HasQuotient.Quotient Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup torsion Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid QuotientGroup.Quotient.commGroup Units.instCommGroupUnits CommRing.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup rank	—	LinearEquiv.finrank_eq RingHomInvPair.ids unitLattice_rank
unitLattice_rank 📖	mathematical	—	Module.finrank dirichletUnitTheorem.logSpace Submodule Int.instSemiring Pi.addCommMonoid NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike unitLattice Submodule.addCommMonoid Submodule.addCommGroup Int.instRing rank	—	finrank_eq_rank ZLattice.rank Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal instDiscrete_unitLattice instZLattice_unitLattice

NumberField.Units.dirichletUnitTheorem

Definitions

Name	Category	Theorems
logSpace 📖	CompOp	30 math math: NumberField.mixedEmbedding.logMap_one, NumberField.Units.finrank_eq_rank, NumberField.Units.logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, NumberField.Units.instZLattice_unitLattice, NumberField.Units.span_basisOfIsMaxRank, NumberField.Units.logEmbeddingQuot_apply, NumberField.Units.basisOfIsMaxRank_apply, map_logEmbedding_sup_torsion, sum_logEmbedding_component, unitLattice_span_eq_top, NumberField.Units.regOfFamily_of_isMaxRank, NumberField.mixedEmbedding.logMap_eq_logEmbedding, unitLattice_inter_ball_finite, logEmbedding_eq_zero_iff, NumberField.Units.instDiscrete_unitLattice, NumberField.mixedEmbedding.logMap_unit_smul, logEmbedding_component, NumberField.Units.logEmbeddingQuot_injective, NumberField.mixedEmbedding.logMap_real, NumberField.Units.unitLattice_rank, NumberField.Units.logEmbeddingEquiv_apply, NumberField.Units.regulator_eq_det', logEmbedding_ker, NumberField.mixedEmbedding.logMap_zero, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.Units.regOfFamily_eq_det', NumberField.mixedEmbedding.logMap_mul, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
seq 📖	CompOp	2 math math: seq_decreasing, seq_norm_le
w₀ 📖	CompOp	51 math math: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.mixedEmbedding.logMap_one, NumberField.mixedEmbedding.fundamentalCone.interior_paramSet, NumberField.Units.finrank_eq_rank, NumberField.Units.logEmbedding_fundSystem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, NumberField.Units.instZLattice_unitLattice, NumberField.Units.span_basisOfIsMaxRank, NumberField.Units.logEmbeddingQuot_apply, NumberField.Units.basisOfIsMaxRank_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, map_logEmbedding_sup_torsion, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, sum_logEmbedding_component, unitLattice_span_eq_top, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, NumberField.Units.regOfFamily_of_isMaxRank, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one, unitLattice_inter_ball_finite, logEmbedding_eq_zero_iff, NumberField.Units.instDiscrete_unitLattice, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, NumberField.mixedEmbedding.logMap_unit_smul, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, logEmbedding_component, NumberField.mixedEmbedding.logMap_apply, NumberField.Units.logEmbeddingQuot_injective, NumberField.mixedEmbedding.logMap_apply_of_norm_one, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', NumberField.mixedEmbedding.logMap_real, NumberField.Units.unitLattice_rank, NumberField.Units.logEmbeddingEquiv_apply, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, NumberField.Units.regulator_eq_det', logEmbedding_ker, NumberField.mixedEmbedding.logMap_zero, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.Units.regOfFamily_eq_det', NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.mixedEmbedding.logMap_mul, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_unit 📖	mathematical	—	Real Real.instLT Real.log DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.instZero	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain mul_comm ENNReal.exists_nat_mul_gt ENNReal.coe_ne_zero NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero ne_of_lt NumberField.mixedEmbedding.minkowskiBound_lt_top Set.Finite.exists_lt_map_eq_of_forall_mem NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt instInfiniteNat Set.mem_setOf_eq Ideal.absNorm_span_singleton Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt seq_norm_le Ideal.finite_setOf_absNorm_le NumberField.RingOfIntegers.instCharZero_1 NumberField.to_charZero Ideal.span_singleton_eq_span_singleton NumberField.RingOfIntegers.instIsDomain Real.log_neg NumberField.Units.pos_at_place map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc inv_mul_cancel₀ seq_ne_zero one_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass NumberField.InfinitePlace.instMonoidWithZeroHomClassReal map_inv₀ mul_inv_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NumberField.InfinitePlace.pos_iff mul_one seq_decreasing
logEmbedding_component 📖	mathematical	—	DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing logSpace AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass NumberField.InfinitePlace w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log NumberField.InfinitePlace.instFunLikeReal RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val	—	—
logEmbedding_component_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm logSpace NormedRing.toNorm Pi.normedRing NumberField.InfinitePlace w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype NormedCommRing.toNormedRing Real.normedCommRing DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding	abs Real.lattice Real.instAddGroup Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	CanLift.prf NNReal.canLift Finset.mem_univ
logEmbedding_eq_zero_iff 📖	mathematical	—	DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing logSpace AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass NumberField.InfinitePlace w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Pi.instZero Real.instZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	—	NumberField.Units.mem_torsion sum_logEmbedding_component Finset.sum_eq_zero mult_log_place_eq_zero neg_eq_zero neg_mul logEmbedding_component Real.log_one MulZeroClass.mul_zero Pi.zero_apply
logEmbedding_ker 📖	mathematical	—	AddMonoidHom.ker Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Additive.addGroup Units.instGroup logSpace Pi.addZeroClass NumberField.InfinitePlace w₀ Real AddMonoid.toAddZeroClass Real.instAddMonoid NumberField.Units.logEmbedding DFunLike.coe OrderIso Subgroup AddSubgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder AddSubgroup.instPartialOrder instFunLikeOrderIso Subgroup.toAddSubgroup NumberField.Units.torsion	—	AddSubgroup.ext AddMonoidHom.mem_ker ofMul_toMul logEmbedding_eq_zero_iff
log_le_of_logEmbedding_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm logSpace NormedRing.toNorm Pi.normedRing NumberField.InfinitePlace w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype NormedCommRing.toNormedRing Real.normedCommRing DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	abs Real.lattice Real.instAddGroup Real.log NumberField.InfinitePlace.instFunLikeReal RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val Real.instMul Real.instNatCast Fintype.card	—	one_mul mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono NumberField.InfinitePlace.mult.eq_1 Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNat_natCast le_rfl Nat.cast_zero sum_logEmbedding_component LE.le.trans le_of_eq norm_sum_le le_trans abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.abs_cast Finset.sum_congr norm_neg norm_mul NormedDivisionRing.toNormMulClass Finset.sum_le_card_nsmul logEmbedding_component_le nsmul_eq_mul Fintype.card_subtype_compl Fintype.card_unique Real.instZeroLEOneClass RCLike.charZero_rclike Nat.instOrderedSub Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Nat.cast_nonneg abs_mul logEmbedding_component Nat.one_le_cast Fintype.card_pos NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed
map_logEmbedding_sup_torsion 📖	mathematical	—	AddSubgroup.map Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Additive.addGroup Units.instGroup logSpace Pi.addGroup NumberField.InfinitePlace w₀ Real Real.instAddGroup NumberField.Units.logEmbedding AddSubgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AddSubgroup.instCompleteLattice DFunLike.coe OrderIso Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder AddSubgroup.instPartialOrder instFunLikeOrderIso Subgroup.toAddSubgroup NumberField.Units.torsion	—	logEmbedding_ker AddSubgroup.map_eq_map_iff sup_right_idem
mult_log_place_eq_zero 📖	mathematical	—	Real Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.instZero Real.instOne	—	mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass NumberField.InfinitePlace.mult_coe_ne_zero Real.log_eq_zero LT.lt.ne' NumberField.Units.pos_at_place Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing NonnegHomClass.apply_nonneg NumberField.InfinitePlace.instNonnegHomClassReal
seq_decreasing 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder NumberField.mixedEmbedding.minkowskiBound Units FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal NumberField.mixedEmbedding.convexBodyLTFactor AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLT DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing seq	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain eq_or_lt_of_le NumberField.to_charZero seq_next Subtype.prop lt_trans
seq_ne_zero 📖	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder NumberField.mixedEmbedding.minkowskiBound Units FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal NumberField.mixedEmbedding.convexBodyLTFactor AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.coe_ne_zero_iff Subtype.prop
seq_next 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder NumberField.mixedEmbedding.minkowskiBound Units FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal NumberField.mixedEmbedding.convexBodyLTFactor AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLT DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal NumberField.RingOfIntegers.val abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.coe_ne_zero_iff Nat.instAtLeastTwoHAddOfNat div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing AbsoluteValue.nonneg Complex.instNontrivial Real.instIsOrderedRing Nonneg.mk_eq_zero div_eq_zero_iff map_eq_zero Real.instNontrivial NumberField.InfinitePlace.instMonoidWithZeroHomClassReal RCLike.charZero_rclike NumberField.to_charZero NumberField.mixedEmbedding.adjust_f NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.mixedEmbedding.convexBodyLT_volume LT.lt.trans div_lt_self NumberField.InfinitePlace.pos_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Rat.cast_le Rat.cast_natCast NumberField.InfinitePlace.prod_eq_abs_norm Finset.prod_le_prod IsOrderedRing.toPosMulMono pow_nonneg IsOrderedRing.toZeroLEOneClass NonnegHomClass.apply_nonneg NumberField.InfinitePlace.instNonnegHomClassReal pow_le_pow_left₀ IsOrderedRing.toMulPosMono LT.lt.le Finset.prod_congr le_of_eq
seq_norm_le 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder NumberField.mixedEmbedding.minkowskiBound Units FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal NumberField.mixedEmbedding.convexBodyLTFactor AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring CommRing.toRing Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing seq	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Mathlib.Tactic.Contrapose.contrapose₁ CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero MulZeroClass.mul_zero ENNReal.instCanonicallyOrderedAdd map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass Nat.cast_le Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero Nat.cast_natAbs Int.cast_abs Rat.instIsStrictOrderedRing NumberField.to_charZero Algebra.coe_norm_int seq_next Subtype.prop
sum_logEmbedding_component 📖	mathematical	—	Finset.sum NumberField.InfinitePlace w₀ Real Real.instAddCommMonoid Finset.univ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype DFunLike.coe AddMonoidHom Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing logSpace AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Real.instMul Real.instNeg Real.instNatCast NumberField.InfinitePlace.mult Real.log NumberField.InfinitePlace.instFunLikeReal RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val	—	NumberField.Units.sum_mult_mul_log Finset.sum_congr neg_mul add_eq_zero_iff_eq_neg add_comm Fintype.sum_eq_add_sum_subtype_ne
unitLattice_inter_ball_finite 📖	mathematical	—	Set.Finite logSpace Set Set.instInter SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid NumberField.InfinitePlace w₀ Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike NumberField.Units.unitLattice Metric.closedBall pseudoMetricSpacePi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero	—	lt_or_ge Metric.closedBall_eq_empty Set.inter_empty Set.finite_empty Set.Finite.of_finite_image Set.Finite.subset NumberField.Embeddings.finite_of_norm_le Complex.isAlgClosed Complex.instCharZero Function.Injective.injOn NumberField.Units.coe_injective Set.Finite.image Subtype.prop NumberField.InfinitePlace.le_iff_le Real.log_le_iff_le_exp NumberField.InfinitePlace.pos_iff NumberField.Units.coe_ne_zero LE.le.trans le_abs_self log_le_of_logEmbedding_le mem_closedBall_zero_iff
unitLattice_span_eq_top 📖	mathematical	—	Submodule.span Real logSpace Real.semiring Pi.addCommMonoid NumberField.InfinitePlace w₀ Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike NumberField.Units.unitLattice Top.top Submodule.instTop	—	le_antisymm le_top Subtype.finite Finite.of_fintype exists_unit Module.Basis.det_apply det_ne_zero_of_sum_col_lt_diag Finset.sum_congr Module.Basis.coePiBasisFun.toMatrix_eq_transpose sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_of_neg mul_neg_of_pos_of_neg IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NumberField.InfinitePlace.mult.eq_1 Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Iff.not Finset.ne_of_mem_erase Finset.sum_neg_distrib sub_neg_eq_add Finset.sum_erase_eq_sub Finset.mem_univ add_comm_sub add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_nonneg le_abs_self sum_logEmbedding_component mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Mathlib.Meta.NormNum.isInt_lt_true Real.instNontrivial Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Subtype.prop Module.Basis.is_basis_iff_det isUnit_iff_ne_zero Submodule.span_monotone

---

← Back to Index