Def uliftZMultiplesHom

Modification history

2025-05-12 07:47

Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean

chore: deduplicate equivalence `M ≃ (ℕ →+ M)` for `M` an additive monoid (#24783) …

Added uliftZMultiplesHom View on Github →