Theorem Zspan.discreteTopology_pi_basisFun

Modification history

2024-09-09 07:09
Mathlib/Algebra/Module/ZLattice/Basic.lean
chore: rename `Zlattice` -> `ZLattice` (#16622) …
Deleted Zspan.discreteTopology_pi_basisFunView on Github →
2024-03-18 10:51
Mathlib/Algebra/Module/Zlattice.lean
chore(*): Fintype -> Finite, drop Decidable (#11423) …
Modified Zspan.discreteTopology_pi_basisFunView on Github →
2023-12-07 17:41
Mathlib/Algebra/Module/Zlattice.lean
feat: add a discrete topology instance for zlattice (#8480) …
Added Zspan.discreteTopology_pi_basisFunView on Github →