rootSet_minpoly_eq_carrier — Mathlib

English

The function c ↦ c.minpoly is injective; equivalently, minpoly_injective holds.

Русский

Функция c ↦ c.minpoly инъективна; эквивалентно справедливости minpoly_injective.

LaTeX

$$$\\text{Injective}(\\,c \\mapsto c.minpoly\\,)$$$

Lean4

theorem rootSet_minpoly_eq_carrier (c : ConjRootClass K L) : c.minpoly.rootSet L = c.carrier :=
  by
  ext x
  rw [mem_carrier, mem_rootSet, aeval_minpoly_iff x c]
  simp [c.minpoly_ne_zero]

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