English
If f: M →* N and x ∈ M has a right inverse y with x y = 1, then f(x) has a right inverse: f(y) with f(x) f(y) = 1.
Русский
Если f: M →* N и у элемента x есть правая обратная, x y = 1, то f(x) имеет правую обратную: f(y) и f(x) f(y) = 1.
LaTeX
$$$\\exists y \\in M: x y = 1 \\Rightarrow \\exists y' \\, (f x) y' = 1 \\, (y' = f y)$$$
Lean4
/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a right inverse,
then `f x` has a right inverse too. For elements invertible on both sides see `IsUnit.map`. -/
@[to_additive /-- Given an AddMonoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
a right inverse, then `f x` has a right inverse too. -/
]
theorem map_exists_right_inv (f : F) {x : M} (hx : ∃ y, x * y = 1) : ∃ y, f x * y = 1 :=
let ⟨y, hy⟩ := hx
⟨f y, map_mul_eq_one f hy⟩
