finrank_map_subtype_eq

Mathlib.LinearAlgebra.Dimension.Finrank

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

← MathLib Explorer

English

For p ⊆ M and q ⊆ p, finrank of q.map p.subtype equals finrank of q.

Русский

Для q ⊆ p ⊆ M вернем Finrank(q.map p.subtype) = Finrank(q).

LaTeX

$$$\\operatorname{finrank}_R (q.map\\ p.subtype) = \\operatorname{finrank}_R q$$$

Lean4

@[simp]
theorem finrank_map_subtype_eq (p : Submodule R M) (q : Submodule R p) : finrank R (q.map p.subtype) = finrank R q :=
  (Submodule.equivSubtypeMap p q).symm.finrank_eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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