finrank_eq_nat_card_basis

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

URI: https://scilib.ai/kg/mathlib#Module.finrank_eq_nat_card_basis

← MathLib Explorer

English

Let b be a basis of a finite module M; if v is linearly independent, then card ι' ≤ card ι.

Русский

Пусть b является базисом конечного модуля M; если v линейно независим, то card ι' ≤ card ι.

LaTeX

$$|\\iota'| \\le |\\iota|$$

Lean4

theorem finrank_eq_nat_card_basis (h : Basis ι R M) : finrank R M = Nat.card ι := by
  rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]

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

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

Разделы

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

Аффилиация

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