involutiveStar — Mathlib

English

There exist trivial star structures on ℕ and ℤ, i.e., star n = n for all n ∈ ℕ and star z = z for all z ∈ ℤ.

Русский

Существуют тривиальные структуры звезды на ℕ и ℤ: star n = n для всех n ∈ ℕ и star z = z для всех z ∈ ℤ.

LaTeX

$$$$ (n : \mathbb{N})^{*} = n \quad \text{and} \quad (z : \mathbb{Z})^{*} = z. $$$$

Lean4

instance involutiveStar {S : Type*} [NonAssocSemiring S] : InvolutiveStar (S →+* R)
    where
  toStar := { star := fun f => RingHom.comp (starRingEnd R) f }
  star_involutive := by
    intro
    ext
    simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]

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