mkQ_apply

Mathlib.LinearAlgebra.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.mkQ_apply

English

The quotient inherits distributive scalar multiplication from S and M, so a • (x + y) = a•x + a•y holds in M/P.

Русский

Фактор-модуль наследует распределение скаляров: a • ([x] + [y]) = a • [x] + a • [y].

LaTeX

$$$\forall a \in S,\forall [x],[y] \in M/P,\ a \cdot \big([x] + [y]\big) = a \cdot [x] + a \cdot [y]$$$

Lean4

@[simp]
theorem mkQ_apply (x : M) : p.mkQ x = Quotient.mk x :=
  rfl

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

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

Разделы

Аффилиация

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