English
Analogous to the previous, for MonoidHom level but in symmetric form.
Русский
Аналогично предыдущему симметричному случаю для моноидных отображений.
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 `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)`. -/
@[to_additive (attr := simp) /-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)`. -/
]
theorem mul_inv {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {x₁ x₂} {y₁ y₂ : S} :
f x₁ * (IsUnit.liftRight (f.restrict S) h y₁)⁻¹ = f x₂ * (IsUnit.liftRight (f.restrict S) h y₂)⁻¹ ↔
f (x₁ * y₂) = f (x₂ * y₁) :=
by rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂, f.map_mul, f.map_mul]
