reflect_eq_zero_iff

Mathlib.Algebra.Polynomial.Reverse

URI: https://scilib.ai/kg/mathlib#Polynomial.reflect_eq_zero_iff

← MathLib Explorer

English

Reflecting a polynomial is zero if and only if the polynomial is zero.

Русский

Reflect нулевой полином равен нулю тогда и только тогда, когда сам полином равен нулю.

LaTeX

$$$\\reflect N f = 0 \\iff f = 0.$$$

Lean4

@[simp]
theorem reflect_eq_zero_iff {N : ℕ} {f : R[X]} : reflect N (f : R[X]) = 0 ↔ f = 0 := by
  rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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