Commit 2024-09-09 07:09 85d6c78a

View on Github →

chore: rename Zlattice -> ZLattice (#16622) Also, with the same logic, the namespace Zspan has be renamed ZSpan.

Estimated changes

added theorem ZLattice.FG
added theorem ZLattice.module_finite
added theorem ZLattice.module_free
added theorem ZLattice.rank
added def ZSpan.ceil
added theorem ZSpan.coe_floor_self
added theorem ZSpan.coe_fract_self
added def ZSpan.floor
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_zSpan_add
added theorem ZSpan.isZLattice
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.span_top
deleted theorem Zlattice.FG
deleted theorem Zlattice.module_finite
deleted theorem Zlattice.module_free
deleted theorem Zlattice.rank
deleted def Zspan.ceil
deleted theorem Zspan.ceil_eq_self_of_mem
deleted theorem Zspan.coe_floor_self
deleted theorem Zspan.coe_fract_self
deleted def Zspan.floor
deleted def Zspan.fract
deleted def Zspan.fractRestrict
deleted theorem Zspan.fractRestrict_apply
deleted theorem Zspan.fract_add_zspan
deleted theorem Zspan.fract_apply
deleted theorem Zspan.fract_eq_fract
deleted theorem Zspan.fract_eq_self
deleted theorem Zspan.fract_fract
deleted theorem Zspan.fract_zspan_add
deleted theorem Zspan.isZlattice
deleted theorem Zspan.norm_fract_le
deleted def Zspan.quotientEquiv
deleted theorem Zspan.repr_ceil_apply
deleted theorem Zspan.repr_floor_apply
deleted theorem Zspan.repr_fract_apply
deleted theorem Zspan.span_top
added theorem ZLattice.covolume_pos
deleted def Zlattice.covolume
deleted theorem Zlattice.covolume_eq_det
deleted theorem Zlattice.covolume_ne_zero
deleted theorem Zlattice.covolume_pos