rootOfSplits'_eq_rootOfSplits — Mathlib

English

rootOfSplits' is definitionally equal to rootOfSplits, after transporting by degree_map.

Русский

rootOfSplits' равен rootOfSplits по определению, после переноса через degree_map.

LaTeX

$$$rootOfSplits'\\; i\\; hf\\; hfd = rootOfSplits\\; i\\; hf\\; (f.\\text{degree\_map } i \\; ▸ \\; hfd).$$$

Lean4

/-- `rootOfSplits'` is definitionally equal to `rootOfSplits`. -/
theorem rootOfSplits'_eq_rootOfSplits {f : K[X]} (hf : f.Splits i) (hfd) :
    rootOfSplits' i hf hfd = rootOfSplits i hf (f.degree_map i ▸ hfd) :=
  rfl

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