finrank_R

Mathlib.FieldTheory.Finite.Polynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.finrank_R

English

For Finite σ, the finite dimension (finrank) of R(σ, K) over K equals card(σ → K).

Русский

Если σ конечно, то финальная размерность R(σ, K) над K равна card(σ → K).

LaTeX

$$$\\\\operatorname{finrank}_K(R(\\\\sigma, K)) = |\\\\sigma \\\\to K|.$$$

Lean4

theorem finrank_R [Fintype σ] : Module.finrank K (R σ K) = Fintype.card (σ → K) :=
  Module.finrank_eq_of_rank_eq (rank_R σ K)

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

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

Разделы

Аффилиация

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