English
For a localization map f with a unit-condition on S, f x1 · (f y1)⁻¹ = f x2 · (f y2)⁻¹ iff f(x1 y2) = f(x2 y1).
Русский
Для отображения локализации f и условия на единицы, равенство двух произведений эквивалентно равенству изображений при перемножении.
LaTeX
$$$f x_1 (f y_1)^{-1} = f x_2 (f y_2)^{-1} \ \Leftrightarrow \ f(x_1 y_2) = f(x_2 y_1).$$$
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 `z = w * (f y)⁻¹ ↔ z * f y = w`. -/
@[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 `z = w - f y ↔ z + f y = w`. -/
]
theorem mul_inv_right {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
z = w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ ↔ z * f y = w := by rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
