pderiv_X_of_ne

Mathlib.Algebra.MvPolynomial.PDeriv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.pderiv_X_of_ne

English

If R is reduced, then IsUnit P iff IsUnit(P_0) and P.totalDegree = 0.

Русский

Если R редуцировано, то IsUnit P эквивалично IsUnit(P_0) и P.totalDegree = 0.

LaTeX

$$$$ [IsReduced(R)] \\Rightarrow \\operatorname{IsUnit}(P) \\iff \\operatorname{IsUnit}(P_0) \\wedge P\\.totalDegree = 0. $$$$

Lean4

@[simp]
theorem pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv i (X j : MvPolynomial σ R) = 0 := by classical simp [h]

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

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

Разделы

Аффилиация

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