Covolume

📁 Source: Mathlib/Algebra/Module/ZLattice/Covolume.lean

Statistics

Metric	Count
Definitions covolume	1
Theorems tendsto_card_div_pow, tendsto_card_div_pow', tendsto_card_div_pow'', tendsto_card_le_div, tendsto_card_le_div', tendsto_card_le_div'', covolume_comap, covolume_div_covolume_eq_relIndex, covolume_div_covolume_eq_relIndex', covolume_eq_det, covolume_eq_det_inv, covolume_eq_det_mul_measureReal, covolume_eq_measure_fundamentalDomain, covolume_ne_zero, covolume_pos, volume_image_eq_volume_div_covolume, volume_image_eq_volume_div_covolume'	17
Total	18

ZLattice

Definitions

Name	Category	Theorems
covolume 📖	CompOp	17 math math: covolume_eq_det_inv, covolume.tendsto_card_div_pow, covolume_div_covolume_eq_relIndex, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.Units.regOfFamily_of_isMaxRank, covolume.tendsto_card_le_div', covolume_eq_measure_fundamentalDomain, covolume_eq_det_mul_measureReal, NumberField.mixedEmbedding.covolume_integerLattice, covolume.tendsto_card_div_pow', volume_image_eq_volume_div_covolume, covolume.tendsto_card_le_div, volume_image_eq_volume_div_covolume', covolume_pos, covolume_comap, covolume_div_covolume_eq_relIndex', covolume_eq_det

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covolume_comap 📖	mathematical	MeasureTheory.MeasurePreserving DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike	covolume comap LinearEquiv.toLinearMap ContinuousLinearEquiv.toLinearEquiv	—	RingHomInvPair.ids instModuleFree_of_discrete_submodule Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real covolume_eq_measure_fundamentalDomain isAddFundamentalDomain Finite.of_fintype instModuleFinite_of_discrete_submodule BorelSpace.opensMeasurable instDiscreteTopologySubtypeMemSubmoduleIntComap instIsZLatticeComap MeasureTheory.MeasurePreserving.measureReal_preimage MeasurableSet.nullMeasurableSet ZSpan.fundamentalDomain_measurableSet ContinuousLinearEquiv.image_symm_eq_preimage ContinuousLinearEquiv.coe_toLinearEquiv ZSpan.map_fundamentalDomain Module.Basis.eq_of_apply_eq Module.Basis.ofZLatticeBasis_apply Module.Basis.ofZLatticeComap_apply
covolume_div_covolume_eq_relIndex 📖	mathematical	Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	DivInvMonoid.toDiv Real.instDivInvMonoid covolume Pi.normedAddCommGroup Real.normedAddCommGroup MeasurableSpace.pi Real.measurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace Real.instNatCast AddSubgroup.relIndex AddCommGroup.toAddGroup Submodule.toAddSubgroup Int.instRing	—	SetLike.coe_mem AddSubgroup.relIndex_eq_natAbs_det Nat.cast_natAbs Int.cast_abs Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal Module.Basis.det_mul_det abs_mul Real.instIsOrderedRing Pi.basisFun_det_apply Module.Basis.isUnit_det Module.Basis.det_inv Units.val_inv_eq_inv_val IsUnit.unit_spec covolume_eq_det mul_comm abs_inv Matrix.ext Module.Basis.ofZLatticeBasis_apply Module.Basis.det_apply Int.cast_det Matrix.map_apply RingHomInvPair.ids Module.Basis.toMatrix_apply Module.Basis.ofZLatticeBasis_repr_apply Submodule.coe_mem
covolume_div_covolume_eq_relIndex' 📖	mathematical	Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	Real DivInvMonoid.toDiv Real.instDivInvMonoid covolume MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace Real.instNatCast AddSubgroup.relIndex AddCommGroup.toAddGroup Submodule.toAddSubgroup Int.instRing	—	RingHomInvPair.ids RingHomCompTriple.ids fact_one_le_two_ennreal MeasureTheory.MeasurePreserving.comp WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal OrthonormalBasis.measurePreserving_repr_symm MeasureTheory.MeasurePreserving.symm Nat.instAtLeastTwoHAddOfNat EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp covolume_comap instIsAddHaarMeasureVolume Pi.borelSpace instCountableFin MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal covolume_div_covolume_eq_relIndex instDiscreteTopologySubtypeMemSubmoduleIntComap instIsZLatticeComap comap_toAddSubgroup RCLike.charZero_rclike LinearEquiv.toAddMonoidHom_commutes AddSubgroup.comap_equiv_eq_map_symm' AddSubgroup.relIndex_map_map_of_injective ContinuousLinearEquiv.injective
covolume_eq_det 📖	mathematical	—	covolume Pi.normedAddCommGroup Real Real.normedAddCommGroup MeasurableSpace.pi Real.measurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace abs Real.lattice Real.instAddGroup Matrix.det Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike Module.Basis Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real FiniteDimensional.proper_real covolume_eq_measure_fundamentalDomain Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace 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 isAddFundamentalDomain Pi.opensMeasurableSpace BorelSpace.opensMeasurable ZSpan.volume_real_fundamentalDomain Module.Basis.ofZLatticeBasis_apply pi_properSpace
covolume_eq_det_inv 📖	mathematical	—	covolume Pi.normedAddCommGroup Real Real.normedAddCommGroup MeasurableSpace.pi Real.measurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.MeasureSpace.pi Real.measureSpace Real.instInv abs Real.lattice Real.instAddGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Module.Basis.equivFun DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finite.of_fintype Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instAddCommGroup FiniteDimensional.rclike_to_real pi_properSpace SeminormedAddGroup.toPseudoMetricSpace instProperSpaceReal	—	RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal covolume_eq_det Pi.basisFun_det_apply Module.Basis.ofZLatticeBasis_apply Module.Basis.isUnit_det Module.Basis.det_inv abs_inv Units.val_inv_eq_inv_val IsUnit.unit_spec Module.Basis.det_basis LinearEquiv.coe_det
covolume_eq_det_mul_measureReal 📖	mathematical	—	covolume Real Real.instMul abs Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Module.Basis Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike MeasureTheory.Measure.real ZSpan.fundamentalDomain Real.linearOrder	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real covolume_eq_measure_fundamentalDomain isAddFundamentalDomain Finite.of_fintype BorelSpace.opensMeasurable ZSpan.measureReal_fundamentalDomain MeasureTheory.measureReal_congr ZSpan.fundamentalDomain_ae_parallelepiped Module.Basis.ofZLatticeBasis_apply
covolume_eq_measure_fundamentalDomain 📖	mathematical	MeasureTheory.IsAddFundamentalDomain Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.zero Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	covolume MeasureTheory.Measure.real	—	AddSubgroup.instMeasurableVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume instCountable_of_discrete_submodule MeasurableVAdd.toMeasurableConstVAdd
covolume_ne_zero 📖	—	—	—	—	instModuleFree_of_discrete_submodule Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real covolume_eq_measure_fundamentalDomain isAddFundamentalDomain Finite.of_fintype instModuleFinite_of_discrete_submodule BorelSpace.opensMeasurable MeasureTheory.measureReal_ne_zero_iff ne_of_lt Bornology.IsBounded.measure_lt_top MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ZSpan.fundamentalDomain_isBounded ZSpan.measure_fundamentalDomain_ne_zero
covolume_pos 📖	mathematical	—	Real Real.instLT Real.instZero covolume	—	lt_of_le_of_ne ENNReal.toReal_nonneg covolume_ne_zero
volume_image_eq_volume_div_covolume 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.image LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.normedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.equivFun Finite.of_fintype Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instAddCommGroup FiniteDimensional.rclike_to_real pi_properSpace SeminormedAddGroup.toPseudoMetricSpace instProperSpaceReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofReal covolume MeasurableSpace.pi Real.measurableSpace	—	RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal LinearEquiv.image_eq_preimage_symm MeasureTheory.Measure.addHaar_preimage_linearEquiv Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace 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 LinearEquiv.symm_symm covolume_eq_det_inv ENNReal.div_eq_inv_mul ENNReal.ofReal_inv_of_pos abs_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Units.ne_zero Real.instNontrivial inv_inv LinearEquiv.coe_det
volume_image_eq_volume_div_covolume' 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike Set.image LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.normedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace Real.instRCLike Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.equivFun Finite.of_fintype Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.proper_real DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofReal covolume	—	Fintype.card_fin Module.finrank_eq_card_basis commRing_strongRankCondition Real.instNontrivial Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real RingHomInvPair.ids RingHomCompTriple.ids fact_one_le_two_ennreal MeasureTheory.MeasurePreserving.comp WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal OrthonormalBasis.measurePreserving_repr_symm PiLp.volume_preserving_toLp MeasureTheory.MeasurePreserving.measure_preimage covolume_comap instIsAddHaarMeasureVolume Pi.borelSpace MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal pi_properSpace instDiscreteTopologySubtypeMemSubmoduleIntComap instIsZLatticeComap volume_image_eq_volume_div_covolume Module.Basis.ofZLatticeBasis_comap ContinuousLinearEquiv.image_symm_eq_preimage Set.image_comp Set.image_congr ContinuousLinearEquiv.apply_symm_apply

ZLattice.covolume

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_card_div_pow 📖	mathematical	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace MeasurableSet MeasurableSpace.pi Real.measurableSpace DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter Set.smulSet Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Monoid.toNatPow Real.instMonoid Fintype.card Filter.atTop Nat.instPreorder nhds MeasureTheory.Measure.real ZLattice.covolume Pi.normedAddCommGroup Real.normedAddCommGroup	—	RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real FiniteDimensional.proper_real pi_properSpace instProperSpaceReal ZLattice.volume_image_eq_volume_div_covolume ENNReal.toReal_div ENNReal.toReal_ofReal LT.lt.le ZLattice.covolume_pos Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace 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 tendsto_card_div_pow'' Pi.topologicalAddGroup instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ENNReal.zero_div
tendsto_card_div_pow' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSet DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instZeroENNReal	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instInv SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Monoid.toNatPow Module.finrank Filter.atTop Nat.instPreorder nhds Real.pseudoMetricSpace MeasureTheory.Measure.real ZLattice.covolume	—	instModuleFree_of_discrete_submodule instModuleFinite_of_discrete_submodule RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition Int.instNontrivial ZLattice.rank ZLattice.volume_image_eq_volume_div_covolume' MeasurableSet.nullMeasurableSet ENNReal.toReal_div ENNReal.toReal_ofReal LT.lt.le ZLattice.covolume_pos instIsAddHaarMeasureVolume tendsto_card_div_pow'' SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasureTheory.NullMeasurableSet.of_null ENNReal.zero_div
tendsto_card_div_pow'' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSet DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.image LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.normedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.equivFun Finite.of_fintype Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.proper_real instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring Real.instInv SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Monoid.toNatPow Fintype.card Filter.atTop Nat.instPreorder nhds MeasureTheory.Measure.real	—	RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real Filter.Tendsto.congr' Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' Nat.card_congr Module.Basis.ofZLatticeBasis_span Set.image_congr EquivLike.toEmbeddingLike Set.mem_inv_smul_set_iff₀ Nat.cast_zero RCLike.charZero_rclike LT.lt.ne' SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass 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 Pi.basisFun_repr tendsto_card_div_pow_atTop_volume NormedSpace.isVonNBounded_iff Bornology.IsVonNBounded.image RingHomSurjective.ids RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace MeasurableEquiv.measurableSet_image
tendsto_card_le_div 📖	mathematical	Set Set.instMembership Real Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instMul Monoid.toNatPow Real.instMonoid Fintype.card Bornology.IsBounded Pi.instBornology PseudoMetricSpace.toBornology Real.pseudoMetricSpace setOf Real.instLE Real.instOne MeasurableSet MeasurableSpace.pi Real.measurableSpace DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter SetLike.coe Submodule Int.instSemiring Pi.addCommMonoid Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup Submodule.setLike Filter.atTop Real.instPreorder nhds MeasureTheory.Measure.real ZLattice.covolume Pi.normedAddCommGroup Real.normedAddCommGroup	—	instModuleFree_of_discrete_submodule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real instModuleFinite_of_discrete_submodule Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition Int.instNontrivial ZLattice.rank Real.instIsStrictOrderedRing instHasSolidNormReal pi_properSpace instProperSpaceReal Module.finrank_fintype_fun_eq_card Real.instNontrivial RingHomInvPair.ids FiniteDimensional.proper_real ZLattice.volume_image_eq_volume_div_covolume ENNReal.toReal_div ENNReal.toReal_ofReal LT.lt.le ZLattice.covolume_pos Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace 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 tendsto_card_le_div'' Pi.topologicalAddGroup instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ENNReal.zero_div
tendsto_card_le_div' 📖	mathematical	Set Set.instMembership Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instMul Monoid.toNatPow Module.finrank Bornology.IsBounded PseudoMetricSpace.toBornology setOf Real.instLE Real.instOne MeasurableSet DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Filter.atTop Real.instPreorder nhds Real.pseudoMetricSpace MeasureTheory.Measure.real ZLattice.covolume	—	instModuleFree_of_discrete_submodule instModuleFinite_of_discrete_submodule RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real ZLattice.volume_image_eq_volume_div_covolume' MeasurableSet.nullMeasurableSet ENNReal.toReal_div ENNReal.toReal_ofReal LT.lt.le ZLattice.covolume_pos instIsAddHaarMeasureVolume tendsto_card_le_div'' Module.nontrivial_of_finrank_pos Int.instNontrivial Module.finrank_pos commRing_strongRankCondition Real.instNontrivial Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors ZLattice.rank Module.Free.instNonemptyChooseBasisIndexOfNontrivial Module.finrank_eq_card_chooseBasisIndex SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasureTheory.NullMeasurableSet.of_null ENNReal.zero_div
tendsto_card_le_div'' 📖	mathematical	Set Set.instMembership Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instMul Monoid.toNatPow Fintype.card Bornology.IsBounded PseudoMetricSpace.toBornology setOf Real.instLE Real.instOne MeasurableSet DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real.measureSpace ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier Pi.topologicalSpace Real.pseudoMetricSpace Set.image LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.equivFun Finite.of_fintype Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.proper_real instZeroENNReal	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Nat.card Set.Elem Set.instInter SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Filter.atTop Real.instPreorder nhds MeasureTheory.Measure.real	—	RingHomInvPair.ids Finite.of_fintype Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real Filter.Tendsto.congr' Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' Nat.cast_ne_zero RCLike.charZero_rclike Fintype.card_ne_zero Real.rpow_pos_of_pos inv_ne_zero LT.lt.ne' lt_iff_le_and_ne Real.rpow_natCast Real.rpow_inv_rpow Nat.card_congr Set.mem_inter_iff Equiv.trans_apply LinearEquiv.coe_toEquiv Equiv.smulRight_apply Real.rpow_neg Set.smul_mem_smul_set_iff₀ Set.mem_smul_set_iff_inv_smul_mem₀ image_smul_set SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Real.rpow_mul inv_mul_cancel₀ Real.rpow_one EquivLike.toEmbeddingLike Module.Basis.ofZLatticeBasis_span Int.instIsDomain 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 Pi.basisFun_repr Filter.Tendsto.comp tendsto_card_div_pow_atTop_volume' NormedSpace.isVonNBounded_iff Bornology.IsVonNBounded.image RingHomSurjective.ids RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace MeasurableEquiv.measurableSet_image Set.image_mono lt_of_lt_of_le le_trans pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono le_of_lt tendsto_rpow_atTop inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos Fintype.card_pos

---

← Back to Index