Basic

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

Statistics

Metric	Count
Definitions IsZLattice, basis, ofZLatticeBasis, ofZLatticeComap, comap, comap_equiv, ceil, floor, fract, fractRestrict, fundamentalDomain, quotientEquiv	12
Theorems isCompact_range_of_periodic, span_top, ofZLatticeBasis_apply, ofZLatticeBasis_comap, ofZLatticeBasis_repr_apply, ofZLatticeBasis_span, ofZLatticeComap_apply, ofZLatticeComap_repr_apply, finrank_eq_int_finrank_of_discrete, coe_comap, comap_comp, comap_discreteTopology, comap_equiv_apply, comap_refl, comap_span_top, comap_toAddSubgroup, isAddFundamentalDomain, module_finite, module_free, rank, ceil_eq_self_of_mem, coe_floor_self, coe_fract_self, discreteTopology_pi_basisFun, exist_unique_vadd_mem_fundamentalDomain, floor_eq_self_of_mem, fractRestrict_apply, fractRestrict_surjective, fract_add_ZSpan, fract_apply, fract_eq_fract, fract_eq_self, fract_fract, fract_mem_fundamentalDomain, fract_zSpan_add, fundamentalDomain_ae_parallelepiped, fundamentalDomain_isBounded, fundamentalDomain_measurableSet, fundamentalDomain_pi_basisFun, fundamentalDomain_reindex, fundamentalDomain_subset_parallelepiped, instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, isAddFundamentalDomain, isAddFundamentalDomain', map, map_fundamentalDomain, measureReal_fundamentalDomain, measure_fundamentalDomain, measure_fundamentalDomain_ne_zero, mem_fundamentalDomain, norm_fract_le, symm_apply, quotientEquiv_apply_mk, repr_ceil_apply, repr_floor_apply, repr_fract_apply, setFinite_inter, smul, span_top, vadd_mem_fundamentalDomain, volume_fundamentalDomain, volume_real_fundamentalDomain, instCountable_of_discrete_submodule, instDiscreteTopologySubtypeMemSubmoduleIntComap, instIsZLatticeComap, instIsZLatticeRealSpan, instModuleFinite_of_discrete_submodule, instModuleFree_of_discrete_submodule	69
Total	81

IsZLattice

Definitions

Name	Category	Theorems
basis 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_range_of_periodic 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	IsCompact Set.range	—	ZLattice.module_free Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real instModuleFinite_of_discrete_submodule le_antisymm RingHomInvPair.ids Finite.of_fintype parallelepiped_basis_eq Module.Basis.repr_symm_apply map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Module.Basis.ofZLatticeBasis_repr_apply Module.Basis.repr_linearCombination covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd add_comm AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass Set.image_subset_range IsCompact.image TopologicalSpace.PositiveCompacts.isCompact
span_top 📖	mathematical	—	Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Top.top Submodule.instTop	—	—

Module.Basis

Definitions

Name	Category	Theorems
ofZLatticeBasis 📖	CompOp	11 math math: ZLattice.covolume_eq_det_inv, ofZLatticeBasis_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, ofZLatticeBasis_span, ZLattice.volume_image_eq_volume_div_covolume, ZLattice.volume_image_eq_volume_div_covolume', ZLattice.isAddFundamentalDomain, ofZLatticeBasis_comap, ofZLatticeBasis_repr_apply, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
ofZLatticeComap 📖	CompOp	3 math math: ofZLatticeComap_apply, ofZLatticeBasis_comap, ofZLatticeComap_repr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofZLatticeBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike ofZLatticeBasis Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.addCommGroup Int.instRing	—	ZLattice.module_free ZLattice.module_finite invariantBasisNumber_of_nontrivial_of_commRing Int.instNontrivial coe_basisOfTopLeSpanOfCardEqFinrank
ofZLatticeBasis_comap 📖	mathematical	—	ofZLatticeBasis ZLattice.comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearEquiv.toLinearEquiv instDiscreteTopologySubtypeMemSubmoduleIntComap instIsZLatticeComap ofZLatticeComap map ContinuousLinearEquiv.symm	—	RingHomInvPair.ids eq_of_apply_eq instDiscreteTopologySubtypeMemSubmoduleIntComap instIsZLatticeComap ofZLatticeBasis_apply ofZLatticeComap_apply
ofZLatticeBasis_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr ofZLatticeBasis Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.addCommMonoid Submodule.addCommGroup Int.instRing	—	RingHomCompTriple.ids LinearMap.CompatibleSMul.finsupp_cod LinearMap.CompatibleSMul.intModule RingHomInvPair.ids ext ofZLatticeBasis_apply repr_self LinearMap.map_zero Finsupp.mapRange_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass DFunLike.congr_fun LinearMap.congr_fun
ofZLatticeBasis_span 📖	mathematical	—	Submodule.span Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule instFunLike ofZLatticeBasis	—	RingHomSurjective.ids Set.ext ofZLatticeBasis_apply Set.image_congr Submodule.map_span Submodule.map.congr_simp span_eq Submodule.map_top Submodule.range_subtype
ofZLatticeComap_apply 📖	mathematical	—	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 ZLattice.comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.addCommGroup Int.instRing instFunLike ofZLatticeComap LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm	—	RingHomInvPair.ids
ofZLatticeComap_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Int.instSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike ZLattice.comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Submodule.addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Submodule.addCommGroup Int.instRing Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr ofZLatticeComap ZLattice.comap_equiv	—	RingHomInvPair.ids LinearEquiv.symm_apply_apply

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_int_finrank_of_discrete 📖	mathematical	—	Set.finrank Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup	—	AddCommGroup.intIsScalarTower RingHomInvPair.ids Submodule.span_le_restrictScalars continuous_of_discreteTopology Isometry.continuous Homeomorph.discreteTopology IsScalarTower.left eq_top_iff LE.le.trans Eq.le Submodule.span_span_coe_preimage Submodule.span_mono Set.preimage_mono Submodule.subset_span Set.finrank.eq_1 LinearEquiv.finrank_eq ZLattice.rank instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_submodule FiniteDimensional.RCLike.properSpace_submodule

ZLattice

Definitions

Name	Category	Theorems
comap 📖	CompOp	13 math math: instIsZLatticeComap, Module.Basis.ofZLatticeComap_apply, comap_discreteTopology, comap_toAddSubgroup, comap_equiv_apply, comap_comp, instDiscreteTopologySubtypeMemSubmoduleIntComap, covolume_comap, Module.Basis.ofZLatticeBasis_comap, Module.Basis.ofZLatticeComap_repr_apply, comap_span_top, coe_comap, comap_refl
comap_equiv 📖	CompOp	2 math math: comap_equiv_apply, Module.Basis.ofZLatticeComap_repr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comap 📖	mathematical	—	SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike comap Set.preimage DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule LinearMap.instFunLike	—	—
comap_comp 📖	mathematical	—	comap LinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids Submodule.comap_comp
comap_discreteTopology 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike	DiscreteTopology Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike comap instTopologicalSpaceSubtype	—	DiscreteTopology.preimage_of_continuous_injective
comap_equiv_apply 📖	mathematical	—	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 comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule DFunLike.coe LinearEquiv Submodule.addCommMonoid Submodule.addCommGroup Int.instRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv comap_equiv LinearEquiv.symm	—	RingHomInvPair.ids
comap_refl 📖	mathematical	—	comap LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Module.End.instOne	—	Submodule.comap_id
comap_span_top 📖	mathematical	Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Top.top Submodule.instTop Set Set.instHasSubset LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	comap	—	RingHomSurjective.ids coe_comap Submodule.span_preimage_eq Submodule.nonempty Submodule.comap_top
comap_toAddSubgroup 📖	mathematical	—	Submodule.toAddSubgroup Int.instRing NormedAddCommGroup.toAddCommGroup AddCommGroup.toIntModule comap AddSubgroup.comap NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup LinearMap.toAddMonoidHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHom.id Semiring.toNonAssocSemiring	—	—
isAddFundamentalDomain 📖	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 ZSpan.fundamentalDomain Real Real.normedField Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.proper_real	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real Module.Basis.ofZLatticeBasis_span ZSpan.isAddFundamentalDomain
module_finite 📖	mathematical	—	Module.Finite 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.addCommMonoid Submodule.addCommGroup Int.instRing	—	Module.Finite.of_fg FG
module_free 📖	mathematical	—	Module.Free 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.addCommMonoid Submodule.addCommGroup Int.instRing	—	module_finite IsStrictOrderedRing.toCharZero IsAddTorsionFree.of_module_rat Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain Int.instIsDomain Ideal.instIsTorsionFreeSubtypeMemSubmodule AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree
rank 📖	mathematical	—	Module.finrank 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.addCommMonoid Submodule.addCommGroup Int.instRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule	—	module_finite IsStrictOrderedRing.toCharZero IsAddTorsionFree.of_module_rat Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain Int.instIsDomain Ideal.instIsTorsionFreeSubtypeMemSubmodule AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree LinearIndependent.map' Module.Basis.linearIndependent Submodule.ker_subtype RingHomSurjective.ids Submodule.map_span Set.range_comp Submodule.map_subtype_top Module.Basis.span_eq Submodule.span_span_of_tower IsZLattice.span_top Set.toFinset_range Finset.card_image_of_injective Subtype.coe_injective Module.Basis.injective Int.instNontrivial Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition le_antisymm exists_linearIndependent Subtype.range_coe_subtype Set.Finite.subset Set.toFinite Finite.Set.finite_range Finite.of_fintype linearIndepOn_id_range_iff Mathlib.Tactic.Contrapose.contrapose₁ Set.setOf_mem_eq Set.toFinset_nonempty Finset.card_le_card Finset.sdiff_eq_empty_iff_subset Set.toFinset_diff LinearEquiv.finrank_eq finrank_span_set_eq_card IsLocalRing.toNontrivial Field.instIsLocalRing LinearIndepOn.eq_1 LinearIndependent.iff_fractionRing Rat.isFractionRing linearIndepOn_id_insert Set.notMem_of_mem_diff Set.mapsTo_inter Set.mapsTo_univ_iff mem_closedBall_zero_iff ZSpan.norm_fract_le sub_mem Submodule.addSubgroupClass zsmul_mem Submodule.subset_span Set.diff_subset Submodule.span_mono Submodule.coe_mem Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete Metric.isBounded_closedBall AddSubgroup.isClosed_of_discrete SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Infinite.exists_ne_map_eq_of_mapsTo Set.infinite_univ Int.infinite Iff.not add_eq_zero_iff_eq_neg Submodule.smul_mem_iff IsScalarTower.rat Submodule.span_subset_span add_smul neg_smul SetLike.mem_coe ZSpan.fract_eq_fract Int.cast_smul_eq_zsmul Mathlib.Tactic.Contrapose.contrapose₄ LinearIndepOn.mono Set.insert_subset Set.mem_of_mem_diff finrank_span_le_card

ZSpan

Definitions

Name	Category	Theorems
ceil 📖	CompOp	2 math math: repr_ceil_apply, ceil_eq_self_of_mem
floor 📖	CompOp	5 math math: floor_eq_self_of_mem, coe_floor_self, vadd_mem_fundamentalDomain, fract_apply, repr_floor_apply
fract 📖	CompOp	11 math math: fractRestrict_apply, fract_fract, norm_fract_le, fract_add_ZSpan, fract_eq_self, fract_mem_fundamentalDomain, repr_fract_apply, fract_zSpan_add, fract_apply, fract_eq_fract, coe_fract_self
fractRestrict 📖	CompOp	3 math math: fractRestrict_apply, quotientEquiv_apply_mk, fractRestrict_surjective
fundamentalDomain 📖	CompOp	32 math math: NumberField.mixedEmbedding.fundamentalDomain_integerLattice, volume_real_fundamentalDomain, fundamentalDomain_measurableSet, fractRestrict_apply, quotientEquiv_apply_mk, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, measureReal_fundamentalDomain, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, volume_fundamentalDomain, measure_fundamentalDomain, isAddFundamentalDomain', fundamentalDomain_reindex, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, exist_unique_vadd_mem_fundamentalDomain, fundamentalDomain_subset_parallelepiped, ZLattice.covolume_eq_det_mul_measureReal, isAddFundamentalDomain, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, fractRestrict_surjective, fract_eq_self, fract_mem_fundamentalDomain, quotientEquiv.symm_apply, fundamentalDomain_isBounded, fundamentalDomain_pi_basisFun, ZLattice.isAddFundamentalDomain, map_fundamentalDomain, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, vadd_mem_fundamentalDomain, mem_fundamentalDomain, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, fundamentalDomain_ae_parallelepiped, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
quotientEquiv 📖	CompOp	2 math math: quotientEquiv_apply_mk, quotientEquiv.symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceil_eq_self_of_mem 📖	mathematical	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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike	ceil	—	Module.Basis.ext_elem RingHomInvPair.ids repr_ceil_apply Module.Basis.mem_span_iff_repr_mem Int.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.ceil_intCast
coe_floor_self 📖	mathematical	—	Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule NormedField.toNormedSpace Module.Basis.instFunLike Module.Basis.singleton floor AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Int.floor	—	Module.Basis.ext_elem RingHomInvPair.ids repr_floor_apply Module.Basis.singleton_repr
coe_fract_self 📖	mathematical	—	fract NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedField.toNormedSpace Module.Basis.singleton DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Int.fract NormedRing.toRing NormedCommRing.toNormedRing	—	Module.Basis.ext_elem RingHomInvPair.ids repr_fract_apply Module.Basis.singleton_repr
discreteTopology_pi_basisFun 📖	mathematical	—	DiscreteTopology Submodule Int.instSemiring Pi.addCommMonoid Real Real.instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Module.Basis Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Module.Basis.instFunLike Pi.basisFun instTopologicalSpaceSubtype Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	nonempty_fintype discreteTopology_iff_isOpen_singleton_zero IsTopologicalAddGroup.toContinuousAdd Submodule.topologicalAddGroup Pi.topologicalAddGroup instIsTopologicalAddGroupReal Metric.isOpen_ball Set.ext Set.mem_preimage mem_ball_zero_iff pi_norm_lt_iff zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.mem_singleton_iff RingHomInvPair.ids Module.Basis.mem_span_iff_repr_mem 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 SetLike.coe_mem Int.cast_abs Real.instIsStrictOrderedRing Int.cast_one Int.cast_lt Int.abs_lt_one_iff Int.cast_eq_zero
exist_unique_vadd_mem_fundamentalDomain 📖	mathematical	—	ExistsUnique 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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike Set Set.instMembership fundamentalDomain HVAdd.hVAdd instHVAdd Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	—	nonempty_fintype AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass vadd_mem_fundamentalDomain
floor_eq_self_of_mem 📖	mathematical	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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike	floor	—	Module.Basis.ext_elem RingHomInvPair.ids repr_floor_apply Module.Basis.mem_span_iff_repr_mem Int.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.floor_intCast
fractRestrict_apply 📖	mathematical	—	Set Set.instMembership fundamentalDomain fractRestrict fract	—	—
fractRestrict_surjective 📖	mathematical	—	Set.Elem fundamentalDomain fractRestrict	—	fract_eq_self Subtype.mem
fract_add_ZSpan 📖	mathematical	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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike	fract AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add_comm fract_zSpan_add
fract_apply 📖	mathematical	—	fract SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike floor	—	—
fract_eq_fract 📖	mathematical	—	fract 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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomInvPair.ids Module.Basis.ext_elem_iff repr_fract_apply Int.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_eq_neg_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass eq_intCast RingHom.instRingHomClass
fract_eq_self 📖	mathematical	—	fract Set Set.instMembership fundamentalDomain	—	RingHomInvPair.ids Module.Basis.ext_elem_iff repr_fract_apply
fract_fract 📖	mathematical	—	fract	—	Module.Basis.ext_elem RingHomInvPair.ids repr_fract_apply Int.fract_fract
fract_mem_fundamentalDomain 📖	mathematical	—	Set Set.instMembership fundamentalDomain fract	—	fract_eq_self fract_fract
fract_zSpan_add 📖	mathematical	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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike	fract AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids Module.Basis.ext_elem_iff repr_fract_apply Int.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.coe_add Pi.add_apply add_tsub_cancel_right AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le eq_intCast RingHom.instRingHomClass Module.Basis.restrictScalars_repr_apply
fundamentalDomain_ae_parallelepiped 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass fundamentalDomain Real Real.normedField Real.linearOrder parallelepiped NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe Module.Basis Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.Basis.instFunLike	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_symmDiff_eq_zero_iff symmDiff_of_le fundamentalDomain_subset_parallelepiped RingHomInvPair.ids parallelepiped_basis_eq le_antisymm Module.Basis.sum_repr Finset.sum_erase_add Finset.mem_univ one_smul vadd_eq_add Set.mem_iUnion AffineSubspace.vadd_mem_mk' Submodule.sum_smul_mem Submodule.subset_span Set.mem_diff_singleton Finset.ne_of_mem_erase MeasureTheory.measure_mono_null MeasureTheory.measure_iUnion_null_iff Finite.to_countable MeasureTheory.Measure.addHaar_affineSubspace AffineSubspace.mem_top Iff.not AffineSubspace.mem_mk' zero_sub AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass linearIndependent_iff_notMem_span Module.Basis.linearIndependent
fundamentalDomain_isBounded 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup fundamentalDomain	—	nonempty_fintype isBounded_iff_forall_norm_le fract_eq_self norm_fract_le
fundamentalDomain_measurableSet 📖	mathematical	—	MeasurableSet fundamentalDomain Real Real.normedField Real.linearOrder	—	nonempty_fintype RingHomInvPair.ids Set.ext measurableSet_preimage Continuous.measurable Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Module.Basis.finiteDimensional_of_finite MeasurableSet.pi Set.countable_univ measurableSet_Ico BorelSpace.opensMeasurable instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
fundamentalDomain_pi_basisFun 📖	mathematical	—	fundamentalDomain Real Real.normedField Pi.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.basisFun Real.semiring Finite.of_fintype Real.linearOrder Set.pi Set.univ Set.Ico Real.instPreorder Real.instZero Real.instOne	—	Set.ext Finite.of_fintype RingHomInvPair.ids Pi.basisFun_repr
fundamentalDomain_reindex 📖	mathematical	—	fundamentalDomain Module.Basis.reindex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	Set.ext RingHomInvPair.ids Module.Basis.repr_reindex Finsupp.mapDomain_equiv_apply Equiv.forall_congr_left
fundamentalDomain_subset_parallelepiped 📖	mathematical	—	Set Set.instHasSubset fundamentalDomain Real Real.normedField Real.linearOrder parallelepiped NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe Module.Basis Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.Basis.instFunLike	—	fundamentalDomain.eq_1 RingHomInvPair.ids parallelepiped_basis_eq Set.setOf_subset_setOf Set.Ico_subset_Icc_self
instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite 📖	mathematical	—	DiscreteTopology AddSubgroup AddCommGroup.toAddGroup NormedAddCommGroup.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike Submodule.toAddSubgroup Int.instRing AddCommGroup.toIntModule Submodule.span Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField Module.Basis.instFunLike instTopologicalSpaceSubtype	—	instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite
instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite 📖	mathematical	—	DiscreteTopology 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.span Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField Module.Basis.instFunLike instTopologicalSpaceSubtype	—	RingHomInvPair.ids SetLike.mem_coe Module.Basis.mem_span_iff_repr_mem 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 DiscreteTopology.of_continuous_injective discreteTopology_pi_basisFun Continuous.restrict continuous_equivFun_basis SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Subtype.map_injective LinearEquiv.injective
isAddFundamentalDomain 📖	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.span Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField Module.Basis.instFunLike Submodule.zero Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor fundamentalDomain Real.linearOrder	—	nonempty_fintype MeasureTheory.IsAddFundamentalDomain.mk' MeasurableSet.nullMeasurableSet fundamentalDomain_measurableSet exist_unique_vadd_mem_fundamentalDomain Real.instIsStrictOrderedRing
isAddFundamentalDomain' 📖	mathematical	—	MeasureTheory.IsAddFundamentalDomain AddSubgroup AddCommGroup.toAddGroup NormedAddCommGroup.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike Submodule.toAddSubgroup Int.instRing AddCommGroup.toIntModule Submodule.span Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField Module.Basis.instFunLike AddSubgroup.zero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid AddSubgroup.normedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddAction.instAddAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor fundamentalDomain Real.linearOrder	—	isAddFundamentalDomain
map 📖	mathematical	—	Submodule.map Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.restrictScalars DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule LinearMap.CompatibleSMul.intModule SeminormedAddCommGroup.toAddCommGroup Submodule.span Set.range DFunLike.coe Module.Basis Module.Basis.instFunLike Module.Basis.map	—	RingHomInvPair.ids RingHomSurjective.ids LinearMap.CompatibleSMul.intModule Submodule.map_span Set.image_congr Set.range_comp
map_fundamentalDomain 📖	mathematical	—	Set.image DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fundamentalDomain Module.Basis.map	—	RingHomInvPair.ids Set.ext mem_fundamentalDomain Module.Basis.map_repr LinearEquiv.trans_apply Set.mem_image_equiv
measureReal_fundamentalDomain 📖	mathematical	—	MeasureTheory.Measure.real fundamentalDomain Real Real.normedField Real.linearOrder Real.instMul abs Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Module.Basis Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.Basis.instFunLike	—	measure_fundamentalDomain ENNReal.toReal_mul ENNReal.toReal_ofReal IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
measure_fundamentalDomain 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike fundamentalDomain Real Real.normedField Real.linearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup AlternatingMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Module.Basis Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.Basis.instFunLike	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype RingHomInvPair.ids Set.eq_preimage_iff_image_eq LinearEquiv.bijective map_fundamentalDomain Module.Basis.map_equiv Equiv.refl_symm Module.Basis.reindex_refl Module.Basis.equiv_symm Module.Basis.det_basis MeasureTheory.Measure.addHaar_preimage_linearEquiv
measure_fundamentalDomain_ne_zero 📖	—	—	—	—	MeasureTheory.IsAddFundamentalDomain.measure_ne_zero Finsupp.instCountableSubtypeMemSubmoduleSpanRange instCountableInt Finite.to_countable MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.instNeZeroOfNonempty MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure AddTorsor.nonempty isAddFundamentalDomain BorelSpace.opensMeasurable
mem_fundamentalDomain 📖	mathematical	—	Set Set.instMembership fundamentalDomain Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing DFunLike.coe Finsupp NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr	—	—
norm_fract_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm fract Finset.sum Real.instAddCommMonoid Finset.univ DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Module.Basis.instFunLike	—	RingHomInvPair.ids Module.Basis.sum_repr Finset.sum_congr repr_fract_apply norm_sum_le norm_smul NormedSpace.toNormSMulClass Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NormOneClass.norm_one NormedDivisionRing.to_normOneClass norm_le_norm_of_abs_le_abs abs_one IsStrictOrderedRing.toIsOrderedRing Int.abs_fract le_of_lt Int.fract_lt_one one_mul mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg
quotientEquiv_apply_mk 📖	mathematical	—	DFunLike.coe Equiv HasQuotient.Quotient Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.hasQuotient Int.instRing Submodule.span Set.range Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike Set.Elem fundamentalDomain EquivLike.toFunLike Equiv.instEquivLike quotientEquiv fractRestrict	—	—
repr_ceil_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Basis Module.Basis.instFunLike ceil AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Int.ceil	—	RingHomInvPair.ids Int.instIsDomain Submodule.coe_sum Finset.sum_congr Module.Basis.restrictScalars_apply Int.cast_smul_eq_zsmul map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.map_smul Module.Basis.repr_self Finsupp.smul_single' mul_one Finset.sum_apply' Finsupp.single_apply Finset.sum_ite_eq'
repr_floor_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Basis Module.Basis.instFunLike floor AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Int.floor	—	RingHomInvPair.ids Int.instIsDomain Submodule.coe_sum Finset.sum_congr Module.Basis.restrictScalars_apply Int.cast_smul_eq_zsmul map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.map_smul Module.Basis.repr_self Finsupp.smul_single' mul_one Finset.sum_apply' Finsupp.single_apply Finset.sum_ite_eq'
repr_fract_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr fract Int.fract NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	RingHomInvPair.ids fract.eq_1 map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.coe_sub Pi.sub_apply repr_floor_apply Int.fract.eq_1
setFinite_inter 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Set.Finite Set Set.instInter SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Submodule.span Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField Module.Basis.instFunLike	—	instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete Submodule.coe_toAddSubgroup AddSubgroup.isClosed_of_discrete SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite
smul 📖	mathematical	—	Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Submodule.pointwiseDistribMulAction Module.toDistribMulAction NormedSpace.toModule AddGroup.int_smulCommClass' NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Submodule.span Set.range DFunLike.coe Module.Basis Module.Basis.instFunLike Module.Basis.isUnitSMul Ne.isUnit DivisionSemiring.toGroupWithZero	—	AddGroup.int_smulCommClass' Ne.isUnit Submodule.smul_span Set.smul_set_range Module.Basis.isUnitSMul_apply
span_top 📖	mathematical	—	Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.coe Submodule Int.instSemiring AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.setLike Set.range DFunLike.coe Module.Basis Module.Basis.instFunLike Top.top Submodule.instTop	—	Submodule.span_span_of_tower AddCommGroup.intIsScalarTower Module.Basis.span_eq
vadd_mem_fundamentalDomain 📖	mathematical	—	Set Set.instMembership fundamentalDomain HVAdd.hVAdd 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.span Set.range DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike instHVAdd Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubgroupClass.toNegMemClass AddGroup.toSubNegMonoid Submodule.addSubgroupClass Int.instRing floor	—	AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass AddLeftCancelSemigroup.toIsLeftCancelAdd NegMemClass.coe_neg sub_eq_add_neg fract_apply fract_zSpan_add Subtype.mem add_comm vadd_eq_add Submodule.vadd_def fract_eq_self
volume_fundamentalDomain 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume fundamentalDomain Real.normedField Pi.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.linearOrder ENNReal.ofReal abs Real.lattice Real.instAddGroup Matrix.det Real.commRing Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Module.Basis Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Module.Basis.instFunLike	—	Finite.of_fintype 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 FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal fundamentalDomain_pi_basisFun MeasureTheory.volume_pi MeasureTheory.Measure.pi_pi Real.volume_Ico sub_zero ENNReal.ofReal_one Finset.prod_const_one mul_one Matrix.det_transpose
volume_real_fundamentalDomain 📖	mathematical	—	MeasureTheory.Measure.real MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real Real.measureSpace MeasureTheory.MeasureSpace.volume fundamentalDomain Real.normedField Pi.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.linearOrder abs Real.lattice Real.instAddGroup Matrix.det Real.commRing DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of Module.Basis Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Module.Basis.instFunLike	—	volume_fundamentalDomain ENNReal.toReal_ofReal IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add

ZSpan.quotientEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem ZSpan.fundamentalDomain HasQuotient.Quotient Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Submodule.hasQuotient Int.instRing Submodule.span Set.range Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule Module.Basis.instFunLike EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ZSpan.quotientEquiv Set Set.instMembership	—	Equiv.symm_apply_eq ZSpan.fractRestrict_apply ZSpan.fract_eq_self Subtype.prop

(root)

Definitions

Name	Category	Theorems
IsZLattice 📖	CompData	7 math math: instIsZLatticeComap, NumberField.Units.instZLattice_unitLattice, instIsZLatticeRealSpan, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, PeriodPair.instIsZLatticeRealComplexLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountable_of_discrete_submodule 📖	mathematical	—	Countable 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	—	instModuleFree_of_discrete_submodule Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.proper_real Module.Basis.ofZLatticeBasis_span Finsupp.instCountableSubtypeMemSubmoduleSpanRange instCountableInt Finite.to_countable Finite.of_fintype instModuleFinite_of_discrete_submodule
instDiscreteTopologySubtypeMemSubmoduleIntComap 📖	mathematical	—	DiscreteTopology 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 ZLattice.comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule ContinuousLinearEquiv.toLinearEquiv instTopologicalSpaceSubtype	—	RingHomInvPair.ids ZLattice.comap_discreteTopology ContinuousLinearEquiv.continuous ContinuousLinearEquiv.injective
instIsZLatticeComap 📖	mathematical	—	IsZLattice ZLattice.comap LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearEquiv.toLinearEquiv instDiscreteTopologySubtypeMemSubmoduleIntComap	—	RingHomInvPair.ids instDiscreteTopologySubtypeMemSubmoduleIntComap ZLattice.coe_comap LinearEquiv.coe_coe ContinuousLinearEquiv.coe_toLinearEquiv ContinuousLinearEquiv.image_symm_eq_preimage RingHomSurjective.ids Submodule.map_span IsZLattice.span_top Submodule.map_top RingHomSurjective.invPair LinearEquiv.range
instIsZLatticeRealSpan 📖	mathematical	—	IsZLattice Real Real.normedField Submodule.span Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule NormedAddCommGroup.toAddCommGroup Set.range DFunLike.coe Module.Basis Real.semiring NormedSpace.toModule Module.Basis.instFunLike ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite	—	ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite ZSpan.span_top
instModuleFinite_of_discrete_submodule 📖	mathematical	—	Module.Finite 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.addCommMonoid Submodule.addCommGroup Int.instRing	—	LinearMap.CompatibleSMul.intModule LinearMap.coe_restrictScalars RingHomSurjective.ids Submodule.map_coe Submodule.map_comap_eq_self LinearMap.mem_range Submodule.subset_span DiscreteTopology.preimage_of_continuous_injective LinearMap.continuous_of_finiteDimensional Submodule.topologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SMulMemClass.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Submodule.smulMemClass Real.instCompleteSpace instT2SpaceSubtype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace FiniteDimensional.finiteDimensional_submodule Submodule.injective_subtype IsScalarTower.left Submodule.map_injective_of_injective Submodule.map_span Submodule.map_top Submodule.range_subtype ZLattice.module_finite Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.RCLike.properSpace_submodule SetLike.ext'_iff Module.Finite.map
instModuleFree_of_discrete_submodule 📖	mathematical	—	Module.Free 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.addCommMonoid Submodule.addCommGroup Int.instRing	—	RCLike.charZero_rclike IsAddTorsionFree.of_module_rat Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain Int.instIsDomain instModuleFinite_of_discrete_submodule Ideal.instIsTorsionFreeSubtypeMemSubmodule AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree

---

← Back to Index