Skip to content

Commit 8ca4eac

Browse files
committed
doc: replace {Add,}MonoidHom.mrange_restrict with {Add,}MonoidHom.mrangeRestrict (leanprover-community#34902)
`{Add,}MonoidHom.mrange_restrict` are old Mathlib3 spellings.
1 parent acb12fd commit 8ca4eac

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Mathlib/Algebra/Group/Submonoid/Operations.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1047,11 +1047,11 @@ def submonoidCongr (h : S = T) : S ≃* T :=
10471047
-- this name is primed so that the version to `f.range` instead of `f.mrange` can be unprimed.
10481048
/-- A monoid homomorphism `f : M →* N` with a left-inverse `g : N → M` defines a multiplicative
10491049
equivalence between `M` and `f.mrange`.
1050-
This is a bidirectional version of `MonoidHom.mrange_restrict`. -/
1050+
This is a bidirectional version of `MonoidHom.mrangeRestrict`. -/
10511051
@[to_additive (attr := simps +simpRhs)
10521052
/-- An additive monoid homomorphism `f : M →+ N` with a left-inverse `g : N → M` defines an
10531053
additive equivalence between `M` and `f.mrange`. This is a bidirectional version of
1054-
`AddMonoidHom.mrange_restrict`. -/]
1054+
`AddMonoidHom.mrangeRestrict`. -/]
10551055
def ofLeftInverse' (f : M →* N) {g : N → M} (h : Function.LeftInverse g f) :
10561056
M ≃* MonoidHom.mrange f :=
10571057
{ f.mrangeRestrict with

0 commit comments

Comments
 (0)