isUnit_iff_mulLeft_bijective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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