Def uliftMultiplesHom

Modification history

2025-05-12 07:47

Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

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

Added uliftMultiplesHom View on Github →