Def Zspan.fundamentalDomain

Modification history

2024-09-09 07:09

Mathlib/Algebra/Module/ZLattice/Basic.lean

chore: rename `Zlattice` -> `ZLattice` (#16622) …

Deleted Zspan.fundamentalDomain View on Github →

2023-06-10 16:28

Mathlib/Algebra/Module/Zlattice.lean

feat: port Algebra.Module.Zlattice (#4944) …

Added Zspan.fundamentalDomain View on Github →