star_snd — Mathlib

English

The star operation on 𝓜(𝕜,A) exchanges the two coordinates with star and flips them: (star a).fst = star ∘ a.snd ∘ star and (star a).snd = star ∘ a.fst ∘ star.

Русский

Оператор звездного преобразования на 𝓜(𝕜,A) меняет координаты местами и применяет звезду: (star a).fst = star ∘ a.snd ∘ star, (star a).snd = star ∘ a.fst ∘ star.

LaTeX

$$$ (\\mathrm{star}\\,a).\\mathrm{fst} = \\mathrm{star} \\circ a.\\mathrm{snd} \\circ \\mathrm{star}, \\; (\\mathrm{star}\\,a).\\mathrm{snd} = \\mathrm{star} \\circ a.\\mathrm{fst} \\circ \\mathrm{star} $$$

Lean4

@[simp]
theorem star_snd (a : 𝓜(𝕜, A)) (b : A) : (star a).snd b = star (a.fst (star b)) :=
  rfl

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