repr_add_sub_repr_add_repr_mem_span

English

Let h be IsAdjoinRoot S f. Then the defect of additivity for repr is controlled by f: the difference h.repr(x+y) − (h.repr x + h.repr y) lies in the span of f.

Русский

Пусть h — IsAdjoinRoot S f. Разность h.repr(x+y) − (h.repr x + h.repr y) принадлежит span{f}.

LaTeX

$$$h.repr(x+y) - \bigl(h.repr(x) + h.repr(y)\bigr) \in \operatorname{span}\{ f \}$$$

Lean4

/-- `repr` preserves addition, up to multiples of `f` -/
theorem repr_add_sub_repr_add_repr_mem_span (x y : S) :
    h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span ({ f } : Set R[X]) := by simp [← h.ker_map]

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