isUnit_iff_mulRight_bijective — Mathlib

English

An element a is a unit if and only if right-multiplication by a is bijective.

Русский

Элемент является единичным тогда и только тогда, когда правое умножение на него является биективным.

LaTeX

$$$$IsUnit(a) \ \iff \text{Bijective}(\lambda x. x\cdot a).$$$$

Lean4

@[to_additive]
theorem isUnit_iff_mulRight_bijective {a : M} : IsUnit a ↔ Function.Bijective (· * a) :=
  ⟨fun h ↦ ⟨h.mul_left_injective, fun y ↦ ⟨y * h.unit⁻¹, by simp [mul_assoc]⟩⟩, fun h ↦
    ⟨⟨a, _, h.1 (by simpa [mul_assoc] using congr_arg (a * ·) (h.2 1).choose_spec), (h.2 1).choose_spec⟩, rfl⟩⟩

Похожие утверждения