ext_elem_iff

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRootMonic.ext_elem_iff

English

ext_elem_iff states x=y iff coefficients match for all i.

Русский

ext_elem_iff утверждает, что x=y тогда и только тогда, когда коэффициенты совпадают для всех i.

LaTeX

$$$ x=y \\iff \\forall i, h.coeff x i = h.coeff y i $$$

Lean4

theorem ext_elem_iff {x y : S} : x = y ↔ ∀ i < natDegree f, h.coeff x i = h.coeff y i :=
  ⟨fun hxy _ _ => hxy ▸ rfl, fun hxy => h.ext_elem hxy⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru