Def uliftPowersHom

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 uliftPowersHom View on Github →