finrank_add_finrank_dualAnnihilator_eq

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Subspace.finrank_add_finrank_dualAnnihilator_eq

← MathLib Explorer

English

For finite-dimensional W ≤ V, dim W + dim W^⊥ = dim V.

Русский

Для конечномерного W ⊆ V выполняется dim W + dim W^⊥ = dim V.

LaTeX

$$finrank K W + finrank K W.dualAnnihilator = finrank K V$$

Lean4

theorem finrank_add_finrank_dualAnnihilator_eq (W : Subspace K V) :
    finrank K W + finrank K W.dualAnnihilator = finrank K V := by
  rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]

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

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

Разделы

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

Аффилиация

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