repr_zero_mem_span — Mathlib

English

If h is IsAdjoinRoot S f, then the image of 0 under repr lies in the ideal generated by f in R[X].

Русский

Если h является IsAdjoinRoot S f, то образ нуля через repr лежит в идеале, порождаемом f в R[X].

LaTeX

$$$h.repr(0) \in \operatorname{span}\{ f \} $$$

Lean4

/-- `repr` preserves zero, up to multiples of `f` -/
theorem repr_zero_mem_span : h.repr 0 ∈ Ideal.span ({ f } : Set R[X]) := by simp [← h.ker_map]

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