English
Under the unit assumption, equality of inverses implies equality of images.
Русский
При условии единичности равенство обратных элементов влечёт равенство изображений.
LaTeX
$$$(f y)^{-1} = (f z)^{-1} \Rightarrow f y = f z$$$
Lean4
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y, z ∈ S`, we have `(f y)⁻¹ = (f z)⁻¹ → f y = f z`. -/
@[to_additive /-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`. -/
]
theorem inv_inj {f : M →* N} (hf : ∀ y : S, IsUnit (f y)) {y z : S}
(h : (IsUnit.liftRight (f.restrict S) hf y)⁻¹ = (IsUnit.liftRight (f.restrict S) hf z)⁻¹) : f y = f z :=
by
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹
