mk_zero

Mathlib.LinearAlgebra.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.Quotient.mk_zero

English

The coset of zero is zero in the quotient; mk 0 equals 0 in M/p.

Русский

Косет нуля в фактор-модуле равен нулю: mk 0 = 0 в M/p.

LaTeX

$$$\operatorname{mk}(0) = 0$$$

Lean4

@[simp]
theorem mk_zero : mk 0 = (0 : M ⧸ p) :=
  rfl

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

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

Разделы

Аффилиация

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