Theorem ZSpan.map

Modification history

2025-04-08 22:12

Mathlib/Algebra/Module/ZLattice/Basic.lean

feat: generalize Mathlib.Algebra.Algebra + Module (#23190) …

Modified ZSpan.map View on Github →

2024-10-21 13:21

Mathlib/Algebra/Module/ZLattice/Basic.lean

feat(Module/ZLattice): define the pullback of a ZLattice (#16822) …

Added ZSpan.map View on Github →