eq_zero_of_eq_zero

Mathlib.Algebra.Polynomial.Basic

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

English

If 0 = 1 in R, then every polynomial p ∈ R[X] equals 0.

Русский

Если 0 = 1 в R, то любой полином p ∈ R[X] равен 0.

LaTeX

$$$0 = 1 \Rightarrow p = 0 \quad\text{for all } p \in R[X]$$$

Lean4

theorem eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : R[X]) : p = 0 := by rw [← one_smul R p, ← h, zero_smul]

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

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

Разделы

Аффилиация

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