Def Zspan.fract_restrict

Modification history

2023-09-07 20:17
Mathlib/Algebra/Module/Zlattice.lean
chore: tidy various files (#7017)
Deleted Zspan.fract_restrictView on Github →
2023-08-20 13:35
Mathlib/Algebra/Module/Zlattice.lean
feat(Algebra.Module.Zlattice): add Zlattice.module_free and Zlattice.rank (#5728) …
Added Zspan.fract_restrictView on Github →