Commit 2023-06-10 16:28 d8ad8d84

View on Github →

feat: port Algebra.Module.Zlattice (#4944) Maybe this file should be called ZLattice....

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Zlattice.lean

added def Zspan.ceil

added theorem Zspan.ceil_eq_self_of_mem

added theorem Zspan.coe_floor_self

added theorem Zspan.coe_fract_self

added theorem Zspan.exist_unique_vadd_mem_fundamentalDomain

added def Zspan.floor

added theorem Zspan.floor_eq_self_of_mem

added def Zspan.fract

added theorem Zspan.fract_add_zspan

added theorem Zspan.fract_apply

added theorem Zspan.fract_eq_fract

added theorem Zspan.fract_eq_self

added theorem Zspan.fract_fract

added theorem Zspan.fract_mem_fundamentalDomain

added theorem Zspan.fract_zspan_add

added def Zspan.fundamentalDomain

added theorem Zspan.fundamentalDomain_bounded

added theorem Zspan.fundamentalDomain_measurableSet

added theorem Zspan.mem_fundamentalDomain

added theorem Zspan.norm_fract_le

added theorem Zspan.repr_ceil_apply

added theorem Zspan.repr_floor_apply

added theorem Zspan.repr_fract_apply

added theorem Zspan.vadd_mem_fundamentalDomain