comapMkQOrderEmbedding_eq

Mathlib.LinearAlgebra.Quotient.Basic

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

English

A simplification: the equality comapMkQOrderEmbedding p p' equals comap p.mkQ p' holds by definition.

Русский

Уравнение comapMkQOrderEmbedding p p' = comap p.mkQ p' следует прямо из определения.

LaTeX

$$$$ comapMkQOrderEmbedding\\; p\\; p' = comap p.mkQ p'. $$$$

Lean4

@[simp]
theorem comapMkQOrderEmbedding_eq (p' : Submodule R (M ⧸ p)) : comapMkQOrderEmbedding p p' = comap p.mkQ p' :=
  rfl

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

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

Разделы

Аффилиация

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