ι_apply — Mathlib

English

The graded embedding ι_Q applied to m coincides with the standard embedding when viewed in the graded structure, i.e., GradedAlgebra.ι Q m equals the direct sum embedding of ι_Q m.

Русский

Градуированное вложение ι_Q(m) совпадает со стандартным вложением в градацию; то есть ι_Q m соответствует прямому сумме через ι_Q.

LaTeX

$$GradedAlgebra.ι_Q(m) = DirectSum.of(…) ι_Q(m)$$

Lean4

theorem ι_apply (m : M) :
    GradedAlgebra.ι Q m = DirectSum.of (fun i => ↥(evenOdd Q i)) 1 ⟨ι Q m, ι_mem_evenOdd_one Q m⟩ :=
  rfl

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