map_subtype_embedding_eq

Mathlib.Algebra.Module.Submodule.Range

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

English

MapSubtype.orderEmbedding p p' equals map p.subtype p'.

Русский

MapSubtype.orderEmbedding p p' равно map p.subtype p'.

LaTeX

$$$$ \mathrm{MapSubtype.orderEmbedding }\; p\; p' = \mathrm{map}\; p.subtype\; p' $$$$

Lean4

@[simp]
theorem map_subtype_embedding_eq (p' : Submodule R p) : MapSubtype.orderEmbedding p p' = map p.subtype p' :=
  rfl

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

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

Разделы

Аффилиация

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