reflect_sub — Mathlib

English

Reflection distributes over subtraction: reflecting the difference f − g equals the difference of reflections.

Русский

Отражение распределяется по вычитанию: отражение разности f − g равно разности отражений.

LaTeX

$$$$\\operatorname{reflect} N (f - g) = \\operatorname{reflect} N f - \\operatorname{reflect} N g.$$$$

Lean4

@[simp]
theorem reflect_sub (f g : R[X]) (N : ℕ) : reflect N (f - g) = reflect N f - reflect N g := by
  rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]

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