mem_unitary_iff_mul_star_self — Mathlib

English

If u is a unit, then u ∈ unitary(R) iff u · star(u) = 1.

Русский

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

LaTeX

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

Lean4

theorem _root_.IsUnit.mem_unitary_iff_mul_star_self {u : R} (hu : IsUnit u) : u ∈ unitary R ↔ u * star u = 1 := by
  rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]

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