natCard_eq_pow_finrank — Mathlib

English

If V is finite over K (Module.Finite), then the natural cardinal of V equals the natural cardinal of K raised to the finite rank of V over K.

Русский

Если V конечно как модуль над K, тогда кардинал NAT(V) равен NAT(K) возведённой в размерность V над K.

LaTeX

$$$ \\mathrm{Nat.card} \\ V = \\mathrm{Nat.card}\\ K ^ \\mathrm{finrank}\\ K\\ V $$$

Lean4

theorem _root_.Module.natCard_eq_pow_finrank [Module.Finite K V] : Nat.card V = Nat.card K ^ finrank K V :=
  by
  let b := IsNoetherian.finsetBasis K V
  rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]

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