star — Mathlib

English

The star operation gives an equivalence on R when star is an involution.

Русский

Операция звезды образует эквивалентность на R, когда она является инвольютивной.

LaTeX

$$$$ \text{star} \,:\, R \to R \text{ is a bijection with } \star(\star r) = r. $$$$

Lean4

/-- `star` as an equivalence when it is involutive. -/
protected def star [InvolutiveStar R] : Equiv.Perm R :=
  star_involutive.toPerm _

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