English
Given f with S such that f(S) ⊆ N×, for all y ∈ S, w,z ∈ N, z = w·f(y)⁻¹ iff z·f(y) = w.
Русский
Если f сопоставляет S под множество единиц и y∈S, то z = w·f(y)⁻¹ эквивалентно z·f(y) = w.
LaTeX
$$$z = w \\cdot (f(y))^{-1} \\iff z \\cdot f(y) = w$ for y ∈ S.$$
Lean4
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`w, z : N` and `y ∈ S`, we have `w * (f y)⁻¹ = z ↔ w = f y * z`. -/
@[to_additive /-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that `f(S) ⊆ AddUnits N`, for all
`w, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`. -/
]
theorem mul_inv_left {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z ↔ w = f y * z :=
by
rw [mul_comm]
exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)
