Commit 2025-03-04 13:59 07e5270f

View on Github →

chore(ZLattice): make ZSpan.isZLattice an instance (#22530)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

deleted theorem ZSpan.isZLattice

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean