Theorem FreeAbelianGroup.liftMonoid_coe_addMonoidHom

Modification history

2026-09-15 17:41
Mathlib/GroupTheory/FreeAbelianGroup.lean
chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …
Deleted FreeAbelianGroup.liftMonoid_coe_addMonoidHomView on Github →
2023-03-14 11:44
Mathlib/GroupTheory/FreeAbelianGroup.lean
feat: port GroupTheory.FreeAbelianGroup (#2247)
Added FreeAbelianGroup.liftMonoid_coe_addMonoidHomView on Github →