coe_starAe — Mathlib

English

The underlying function of the starAe is the composition op ∘ star; i.e., applying starAe to an element equals applying star and then taking its opposite.

Русский

Функция starAe на уровне отображения равна композиции op ∘ star; то есть применение starAe к элементу эквивалентно применению star и взятию противоположного.

LaTeX

$$$\text{coe}(\text{starAe}) = \mathrm{op} \circ \star$$$

Lean4

@[simp]
theorem coe_starAe : ⇑(starAe : ℍ[R,c₁,c₂,c₃] ≃ₐ[R] _) = op ∘ star :=
  rfl

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