mem_iff_star_mul_self — Mathlib

English

Let R be a commutative monoid with an involution *. An element U ∈ R is unitary if and only if star(U) · U = 1.

Русский

Пусть R — коммутативный моноид с инволюцией *. Элемент U ∈ R проступает как унитарный тогда и только тогда star(U) · U = 1.

LaTeX

$$$U \in \mathrm{Unitary}(R) \iff \star U \cdot U = 1$$$

Lean4

theorem mem_iff_star_mul_self {U : R} : U ∈ unitary R ↔ star U * U = 1 :=
  mem_iff.trans <| and_iff_left_of_imp fun h => mul_comm (star U) U ▸ h

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