mem_iff_self_mul_star — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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