mem_unitary_iff_star_mul_self — Mathlib

English

If u is a unit of R, then u is unitary in R if and only if star(u) · u = 1.

Русский

Если u является единицей в R, то u ∈ unitary(R) тогда и только тогда, когда star(u) · u = 1.

LaTeX

$$$ u \in \mathrm{Unitary}(R) \iff \star u \cdot u = 1 \,(\text{для } \mathrm{IsUnit}(u)) $$$

Lean4

theorem _root_.IsUnit.mem_unitary_iff_star_mul_self {u : R} (hu : IsUnit u) : u ∈ unitary R ↔ star u * u = 1 :=
  by
  rw [unitary.mem_iff, and_iff_left_of_imp fun h_mul => ?_]
  lift u to Rˣ using hu
  exact left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv

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