ι_mul_ι_mem_evenOdd_zero — Mathlib

English

For any m1,m2 ∈ M, the product ι_Q(m1) ι_Q(m2) belongs to the degree-0 (even) component of the parity grading: ι_Q(m1) ι_Q(m2) ∈ evenOdd(Q,0).

Русский

Для любых m1,m2 ∈ M произведение ι_Q(m1) ι_Q(m2) лежит в компоненте градации чётной части: ι_Q(m1) ι_Q(m2) ∈ evenOdd(Q,0).

LaTeX

$$$ι_Q(m_1) ι_Q(m_2) \\in \\mathrm{evenOdd}(Q,0)$$$

Lean4

theorem ι_mul_ι_mem_evenOdd_zero (m₁ m₂ : M) : ι Q m₁ * ι Q m₂ ∈ evenOdd Q 0 :=
  Submodule.mem_iSup_of_mem ⟨2, rfl⟩
    (by
      rw [Subtype.coe_mk, pow_two]
      exact Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁) (LinearMap.mem_range_self (ι Q) m₂))

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