Def OrderAddMonoidIso.toMultiplicativeLeft

Modification history

2025-10-08 17:24

Mathlib/Algebra/Order/Hom/TypeTags.lean

chore: rename `MonoidHom.toAdditive''` to `MonoidHom.toAdditiveLeft` (#29800) …

Added OrderAddMonoidIso.toMultiplicativeLeft View on Github →