comp_removeZero — Mathlib

English

Removing the zero coefficient from a composition q ∘ p does not change the resulting composition, provided the zero coefficient is handled appropriately.

Русский

Удаление нулевого коэффициента из композиции q∘p не меняет результат композиции, если нулевой коэффициент корректно учтен.

LaTeX

$$$q.removeZero.comp p = q.comp p$.$$

Lean4

@[simp]
theorem comp_removeZero (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
    q.comp p.removeZero = q.comp p := by ext n; simp [FormalMultilinearSeries.comp]

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