mk_self

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.mk_self

English

The image of the root under mk f is zero: mk f (root f) = 0.

Русский

Изображение корня под mk f равно нулю: mk f (root f) = 0.

LaTeX

$$mk f f = 0$$

Lean4

@[simp]
theorem mk_self : mk f f = 0 :=
  Quotient.sound' <| QuotientAddGroup.leftRel_apply.mpr (mem_span_singleton.2 <| by simp)

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

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

Разделы

Аффилиация

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