rank_eq_lift — Mathlib

English

For a type σ and a field K, the K-rank (dimension) of the multivariate polynomial ring MvPolynomial(σ,K) equals the lifted cardinal of the set of finitely supported functions σ → ℕ.

Русский

Для типа σ и поля K размерность (ранг) K-многочленовой алгебры MvPolynomial(σ,K) равна поднятой кардинальности множества функций с конечной опорой σ → ℕ.

LaTeX

$$$\\operatorname{Module.rank}_K\\bigl( \\mathrm{MvPolynomial}(\\sigma,K) \\bigr) = \\operatorname{lift} \\bigl( \\#(\\sigma \\to_0 \\mathbb{N}) \\bigr)$.$$

Lean4

theorem rank_eq_lift : Module.rank K (MvPolynomial σ K) = lift.{v} #(σ →₀ ℕ) := by
  rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]

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