mk_add

Mathlib.LinearAlgebra.Quotient.Defs

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

English

The operation on cosets respects addition: mk(x+y) = mk x + mk y.

Русский

Операция над косетами сохраняет сложение: mk(x+y) = mk x + mk y.

LaTeX

$$$\operatorname{mk}(x+y) = \operatorname{mk}(x) + \operatorname{mk}(y).$$$

Lean4

@[simp]
theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y :=
  rfl

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

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

Разделы

Аффилиация

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