English
If f: M →* N and x ∈ M has a left inverse y with y x = 1, then f(x) has a left inverse: y' with y' f(x) = 1.
Русский
Если f: M →* N и у x есть левая обратная y, y x = 1, то f(x) имеет левую обратную: y' с y' f(x) = 1.
LaTeX
$$$\\exists y \\; y x = 1 \\Rightarrow \\exists y' \\, y' f x = 1$$$
Lean4
/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a left inverse,
then `f x` has a left 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 left inverse, then `f x` has a left inverse too. For elements invertible on both sides see
`IsAddUnit.map`. -/
]
theorem map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) : ∃ y, y * f x = 1 :=
let ⟨y, hy⟩ := hx
⟨f y, map_mul_eq_one f hy⟩
