id_comp' — Mathlib

English

A variant of id_comp: If the zero coefficient in id 𝕜 F x equals p 0 v0, then (id 𝕜 F x).comp p = p.

Русский

Вариант id_comp': если нулевой коэффициент id 𝕜 F x задаётся равенством x = p 0 v0, то (id 𝕜 F x).comp p = p.

LaTeX

$$$(id\\ 𝕜\\ F x).comp\\ p = p$ when $x = p 0 v0$.$$

Lean4

/-- Variant of `id_comp` in which the zero coefficient is given by an equality hypothesis instead
of a definitional equality. Useful for rewriting or simplifying out in some situations. -/
theorem id_comp' (p : FormalMultilinearSeries 𝕜 E F) (x : F) (v0 : Fin 0 → E) (h : x = p 0 v0) :
    (id 𝕜 F x).comp p = p := by simp [h]

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