Regulator

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

Statistics

Metric	Count
Definitions IsMaxRank, basisOfIsMaxRank, equivFinRank, regOfFamily, regulator	5
Theorems abs_det_eq_abs_det, basisOfIsMaxRank_apply, basisOfIsMaxRank_fundSystem, finiteIndex_iff_sup_torsion_finiteIndex, finrank_mul_regOfFamily_eq_det, finrank_mul_regulator_eq_det, isMaxRank_fundSystem, isMaxRank_iff_closure_finiteIndex, regOfFamily_div_regOfFamily, regOfFamily_div_regulator, regOfFamily_eq_det, regOfFamily_eq_det', regOfFamily_eq_zero, regOfFamily_ne_zero, regOfFamily_ne_zero_iff, regOfFamily_of_isMaxRank, regOfFamily_pos, regulator_eq_det, regulator_eq_det', regulator_eq_regOfFamily_fundSystem, regulator_ne_zero, regulator_pos, span_basisOfIsMaxRank	23
Total	28

NumberField.Units

Definitions

Name	Category	Theorems
IsMaxRank 📖	MathDef	3 math math: isMaxRank_fundSystem, regOfFamily_ne_zero_iff, isMaxRank_iff_closure_finiteIndex
basisOfIsMaxRank 📖	CompOp	4 math math: span_basisOfIsMaxRank, basisOfIsMaxRank_apply, regOfFamily_of_isMaxRank, basisOfIsMaxRank_fundSystem
equivFinRank 📖	CompOp	2 math math: regulator_eq_det', regOfFamily_eq_det'
regOfFamily 📖	CompOp	10 math math: regOfFamily_eq_det, finrank_mul_regOfFamily_eq_det, regOfFamily_of_isMaxRank, regOfFamily_div_regulator, regOfFamily_div_regOfFamily, regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det', regOfFamily_eq_zero, NumberField.IsCMField.regOfFamily_realFunSystem, regOfFamily_pos
regulator 📖	CompOp	16 math math: NumberField.dedekindZeta_residue_def, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv, regulator_eq_det, regOfFamily_div_regulator, NumberField.Ideal.tendsto_norm_le_div_atTop₀, regulator_pos, NumberField.Ideal.tendsto_norm_le_div_atTop, regulator_eq_regOfFamily_fundSystem, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, finrank_mul_regulator_eq_det, regulator_eq_det', NumberField.IsCMField.regOfFamily_realFunSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_det_eq_abs_det 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log 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 rank	—	EquivLike.toEmbeddingLike Matrix.det_permute one_mul Int.cast_one Equiv.Perm.sign_abs Int.cast_abs Real.instIsStrictOrderedRing abs_mul Real.instIsOrderedRing Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' Finset.sum_congr Real.log_prod pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass map_ne_zero Real.instNontrivial NumberField.InfinitePlace.instMonoidWithZeroHomClassReal coe_ne_zero Equiv.prod_comp NumberField.to_charZero NumberField.InfinitePlace.prod_eq_abs_norm norm Rat.cast_one Real.log_one Matrix.det_reindex_self Matrix.ext Equiv.apply_symm_apply finSuccEquiv_succ one_smul Int.abs_negOnePow abs_zsmul Real.instIsOrderedAddMonoid Units.smul_def
basisOfIsMaxRank_apply 📖	mathematical	IsMaxRank	DFunLike.coe Module.Basis rank 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 Module.Basis.instFunLike basisOfIsMaxRank 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 logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	Module.Basis.coe_reindex coe_basisOfPiSpaceOfLinearIndependent Equiv.symm_apply_apply
basisOfIsMaxRank_fundSystem 📖	mathematical	—	basisOfIsMaxRank fundSystem isMaxRank_fundSystem Module.Basis.ofZLatticeBasis Real Real.normedField Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing 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 FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Subtype.finite Finite.of_fintype Real.instAddCommGroup NormedSpace.toModule FiniteDimensional.rclike_to_real pi_properSpace SeminormedAddGroup.toPseudoMetricSpace instProperSpaceReal unitLattice instDiscrete_unitLattice rank instZLattice_unitLattice basisUnitLattice	—	Module.Basis.eq_of_apply_eq isMaxRank_fundSystem Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal instDiscrete_unitLattice instZLattice_unitLattice Module.Basis.ofZLatticeBasis_apply basisOfIsMaxRank_apply logEmbedding_fundSystem
finiteIndex_iff_sup_torsion_finiteIndex 📖	mathematical	—	Subgroup.FiniteIndex Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Subgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice torsion	—	Subgroup.finiteIndex_of_le le_sup_left Subgroup.finiteIndex_iff Subgroup.relIndex_mul_index Subgroup.relIndex_sup_left Subgroup.normal_of_comm Subgroup.FiniteIndex.index_ne_zero Subgroup.finiteIndex_of_finite Finite.of_fintype
finrank_mul_regOfFamily_eq_det 📖	mathematical	—	Real Real.instMul Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero regOfFamily abs Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of NumberField.InfinitePlace.mult Real.log NumberField.InfinitePlace.instFunLikeReal RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero rank	—	EquivLike.toEmbeddingLike NumberField.to_charZero Matrix.det_reindex_self Matrix.det_eq_sum_row_mul_submatrix_succAbove_succAbove_det Equiv.forall_congr_left Equiv.sum_comp Finset.sum_congr Equiv.apply_symm_apply Finset.sum_dite_irrel sum_mult_mul_log abs_mul Real.instIsOrderedRing abs_neg_one_pow one_mul Matrix.det.congr_simp Matrix.submatrix_submatrix NumberField.InfinitePlace.sum_mult_eq Nat.abs_cast regOfFamily_eq_det Matrix.ext Matrix.reindex_apply Matrix.submatrix_apply Matrix.of_apply
finrank_mul_regulator_eq_det 📖	mathematical	—	Real Real.instMul Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero regulator abs Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of NumberField.InfinitePlace.mult Real.log NumberField.InfinitePlace.instFunLikeReal RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero fundSystem rank	—	NumberField.to_charZero regulator_eq_regOfFamily_fundSystem finrank_mul_regOfFamily_eq_det
isMaxRank_fundSystem 📖	mathematical	—	IsMaxRank fundSystem	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal instDiscrete_unitLattice instZLattice_unitLattice logEmbedding_fundSystem Module.Basis.ofZLatticeBasis_apply Module.Basis.linearIndependent
isMaxRank_iff_closure_finiteIndex 📖	mathematical	—	IsMaxRank Subgroup.FiniteIndex Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Subgroup.closure Set.range rank	—	RingHomInvPair.ids AddSubgroup.index_ne_zero_iff_finite Subgroup.normal_of_comm Subgroup.index_map mul_one Subgroup.index_top QuotientGroup.range_mk' QuotientGroup.ker_mk' Subgroup.index_toAddSubgroup AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddSubgroup.index_map_equiv Set.range_comp LinearEquiv.coe_coe RingHomSurjective.ids Submodule.map_span DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.map_toAddSubgroup Submodule.span_int_eq_addSubgroupClosure MonoidHom.map_closure Subgroup.toAddSubgroup_closure QuotientGroup.coe_mk' Equiv.image_symm_eq_preimage SetLike.isDiscrete_iff_discreteTopology IsDiscrete.mono DiscreteTopology.isDiscrete instDiscrete_unitLattice SetLike.coe_subset_coe instIsConcreteLE Submodule.span_le Submodule.mem_top finiteIndex_iff_sup_torsion_finiteIndex Subgroup.finiteIndex_iff Submodule.finiteQuotient_iff instModuleFree_of_discrete_submodule FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real instModuleFinite_of_discrete_submodule unitLattice_rank Set.finrank.eq_1 IsMaxRank.eq_1 linearIndependent_iff_card_eq_finrank_span CommRing.orzechProperty Real.instNontrivial Real.finrank_eq_int_finrank_of_discrete Submodule.finrank_map_subtype_eq Set.range_comp' Fintype.card_fin
regOfFamily_div_regOfFamily 📖	mathematical	IsMaxRank Subgroup Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.closure Set.range rank torsion	Real DivInvMonoid.toDiv Real.instDivInvMonoid regOfFamily Real.instNatCast Subgroup.relIndex	—	Submodule.toAddSubgroup_le span_basisOfIsMaxRank dirichletUnitTheorem.map_logEmbedding_sup_torsion SupHomClass.map_sup SupBotHomClass.toSupHomClass sSupHomClass.toSupBotHomClass OrderIsoClass.tosSupHomClass OrderIso.instOrderIsoClass AddSubgroup.map_mono OrderIso.le_iff_le regOfFamily_of_isMaxRank ZLattice.covolume_div_covolume_eq_relIndex ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Finite.of_fintype instIsZLatticeRealSpan AddSubgroup.relIndex_map_map dirichletUnitTheorem.logEmbedding_ker OrderIso.map_sup Subgroup.relIndex_toAddSubgroup regOfFamily_eq_zero zero_div Nat.cast_eq_zero RCLike.charZero_rclike Subgroup.finiteIndex_iff finiteIndex_iff_sup_torsion_finiteIndex isMaxRank_iff_closure_finiteIndex mul_eq_zero_iff_right IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Subgroup.relIndex_mul_index Subgroup.not_finiteIndex_iff Iff.not
regOfFamily_div_regulator 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid regOfFamily regulator Real.instNatCast Subgroup.index Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Subgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.closure Set.range rank torsion	—	regulator_eq_regOfFamily_fundSystem regOfFamily_div_regOfFamily isMaxRank_fundSystem closure_fundSystem_sup_torsion_eq_top Subgroup.relIndex_top_right
regOfFamily_eq_det 📖	mathematical	—	regOfFamily abs Real Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log 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 rank	—	regOfFamily_eq_det' abs_det_eq_abs_det
regOfFamily_eq_det' 📖	mathematical	—	regOfFamily abs Real Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace dirichletUnitTheorem.w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of 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 AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbedding Additive.ofMul rank Equiv.symm equivFinRank	—	regOfFamily_of_isMaxRank Int.instIsDomain Real.instNontrivial AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add ZLattice.covolume_eq_det ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Finite.of_fintype instIsZLatticeRealSpan Module.Basis.coe_reindex Module.Basis.restrictScalars_apply basisOfIsMaxRank_apply regOfFamily_eq_zero Matrix.det_eq_zero_of_not_linearIndependent_rows Real.instIsDomain linearIndependent_equiv IsMaxRank.eq_1 abs_zero
regOfFamily_eq_zero 📖	mathematical	IsMaxRank	regOfFamily Real Real.instZero	—	regOfFamily.eq_1
regOfFamily_ne_zero 📖	—	IsMaxRank	—	—	LT.lt.ne' regOfFamily_pos
regOfFamily_ne_zero_iff 📖	mathematical	—	IsMaxRank	—	Function.mt regOfFamily_eq_zero regOfFamily_ne_zero
regOfFamily_of_isMaxRank 📖	mathematical	IsMaxRank	regOfFamily ZLattice.covolume dirichletUnitTheorem.logSpace Pi.normedAddCommGroup NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup MeasurableSpace.pi Real.measurableSpace Submodule.span Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Set.range rank DFunLike.coe Module.Basis Real.semiring Pi.addCommMonoid 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 Module.Basis.instFunLike basisOfIsMaxRank MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace	—	regOfFamily.eq_1
regOfFamily_pos 📖	mathematical	IsMaxRank	Real Real.instLT Real.instZero regOfFamily	—	regOfFamily_of_isMaxRank ZLattice.covolume_pos FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite instIsZLatticeRealSpan MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal
regulator_eq_det 📖	mathematical	—	regulator abs Real Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log 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 fundSystem rank	—	regulator_eq_regOfFamily_fundSystem regOfFamily_eq_det
regulator_eq_det' 📖	mathematical	—	regulator abs Real Real.lattice Real.instAddGroup Matrix.det NumberField.InfinitePlace dirichletUnitTheorem.w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of 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 AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logEmbedding Additive.ofMul fundSystem rank Equiv.symm equivFinRank	—	regulator_eq_regOfFamily_fundSystem regOfFamily_eq_det'
regulator_eq_regOfFamily_fundSystem 📖	mathematical	—	regulator regOfFamily fundSystem	—	isMaxRank_fundSystem regOfFamily_of_isMaxRank regulator.eq_1 Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal instDiscrete_unitLattice instZLattice_unitLattice Module.Basis.ofZLatticeBasis_span basisOfIsMaxRank_fundSystem
regulator_ne_zero 📖	—	—	—	—	LT.lt.ne' regulator_pos
regulator_pos 📖	mathematical	—	Real Real.instLT Real.instZero regulator	—	regOfFamily_pos isMaxRank_fundSystem regulator_eq_regOfFamily_fundSystem
span_basisOfIsMaxRank 📖	mathematical	IsMaxRank	Submodule.toAddSubgroup dirichletUnitTheorem.logSpace Int.instRing Pi.addCommGroup NumberField.InfinitePlace dirichletUnitTheorem.w₀ Real Real.instAddCommGroup AddCommGroup.toIntModule Submodule.span Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid Set.range rank DFunLike.coe Module.Basis Real.semiring Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.instFunLike basisOfIsMaxRank AddSubgroup.map Additive Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Additive.addGroup Units.instGroup Pi.addGroup Real.instAddGroup logEmbedding OrderIso Subgroup AddSubgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder AddSubgroup.instPartialOrder instFunLikeOrderIso Subgroup.toAddSubgroup Subgroup.closure	—	Subgroup.toAddSubgroup_closure AddMonoidHom.map_closure Submodule.span_int_eq_addSubgroupClosure Set.ext basisOfIsMaxRank_apply Set.image_congr

---

← Back to Index