mem_roots'

Mathlib.Algebra.Polynomial.Roots

URI: https://scilib.ai/kg/mathlib#Polynomial.mem_roots'

English

For hp ≠ 0, a ∈ p.roots iff IsRoot p a.

Русский

Для hp ≠ 0, a ∈ p.roots тогда и только тогда, когда IsRoot p a.

LaTeX

$$∀ {p : Polynomial R}, h ≠ 0 → a ∈ p.roots ↔ IsRoot p a$$

Lean4

@[simp]
theorem mem_roots' : a ∈ p.roots ↔ p ≠ 0 ∧ IsRoot p a := by
  classical rw [← count_pos, count_roots p, rootMultiplicity_pos']

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

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

Разделы

Аффилиация

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