coe_starAe

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.coe_starAe

English

The underlying function of starAe equals op ∘ star.

Русский

Базовая функция starAe равна op ∘ star.

LaTeX

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

Lean4

@[simp]
theorem coe_starAe : ⇑(starAe : ℍ[R] ≃ₐ[R] ℍ[R]ᵐᵒᵖ) = op ∘ star :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru