mul_div_root_cancel — Mathlib

English

In AdjoinRoot f, the identity (X − root f) · ((f.map (of f)) / (X − root f)) = f.map (of f) expresses that X − root f divides f.map (of f) with remainder zero.

Русский

В AdjoinRoot f выражение (X − root f) · ((f.map (of f)) / (X − root f)) = f.map (of f) говорит, что X − root f делит f.map (of f) без остатка.

LaTeX

$$(X - root f) * (f.map (of f) / (X - root f)) = f.map (of f)$$

Lean4

theorem mul_div_root_cancel [Fact (Irreducible f)] :
    (X - C (root f)) * ((f.map (of f)) / (X - C (root f))) = f.map (of f) :=
  (isRoot_root _).mul_div_eq

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