changeForm_ι_mul_ι — Mathlib

English

Applying changeForm to the product ι_Q(m1) * ι_Q(m2) yields the product ι_Q'(m1) * ι_Q'(m2) minus the scalar algebra map of B(m1,m2).

Русский

Применение changeForm к произведению ι_Q(m1) * ι_Q(m2) даёт ι_Q'(m1) * ι_Q'(m2) минус алгебраическую карту скаляра B(m1,m2).

LaTeX

$$$ changeForm(h)(\iota_Q(m_1) * \iota_Q(m_2)) = \iota_{Q'}(m_1) * \iota_{Q'}(m_2) - \text{algebraMap}(B(m_1,m_2)) $$$

Lean4

theorem changeForm_ι_mul_ι (m₁ m₂ : M) :
    changeForm h (ι Q m₁ * ι Q m₂) = ι Q' m₁ * ι Q' m₂ - algebraMap _ _ (B m₁ m₂) := by
  rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι]

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