associated_one_iff_isUnit — Mathlib

English

In a monoid M, (a) is associated with 1 iff a is a unit.

Русский

В моноиде M, a ~ᵤ 1 тогда и только тогда, когда a является единицей.

LaTeX

$$$ (a : M) ~ᵤ 1 \\iff IsUnit\\ a. $$$

Lean4

@[simp]
theorem associated_one_iff_isUnit [Monoid M] {a : M} : (a : M) ~ᵤ 1 ↔ IsUnit a :=
  Iff.intro
    (fun h =>
      let ⟨c, h⟩ := h.symm
      h ▸ ⟨c, (one_mul _).symm⟩)
    fun ⟨c, h⟩ => Associated.symm ⟨c, by simp [h]⟩

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