ne_zero

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.Monic.ne_zero

English

The unit element 1 in R[A] is monic with respect to D whenever D is injective.

Русский

Единственный элемент единицы в R[A] является моничным относительно D при инъективности D.

LaTeX

$$(1 : R[A]).Monic D$$

Lean4

theorem ne_zero [Nonempty A] [Nontrivial R] (hp : p.Monic D) : p ≠ 0 := fun h => by
  simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp

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

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

Разделы

Аффилиация

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