monic_one

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.monic_one

English

The same fact: the unit element is monic with respect to D when D is injective.

Русский

Та же самая характеристика: единица монична относительно D при инъективности D.

LaTeX

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

Lean4

@[simp]
theorem monic_one [AddZeroClass A] (hD : D.Injective) : (1 : R[A]).Monic D := by
  rw [Monic, one_def, leadingCoeff_single hD]

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

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

Разделы

Аффилиация

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