Mathlib Map

Theorems · Theorem · number theory

MvPolynomial.finrank_R

∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ],
  Module.finrank K (MvPolynomial.R σ K) = Fintype.card (σ → K)
Defined in
Mathlib.FieldTheory.Finite.Polynomial
Cited by
1 results in Mathlib
Foundations
Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeFieldFintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MvPolynomial.ker_evalₗ · cited by 1MvPolynomial.ker_evalₗFintype · cited by 7736FintypeField · cited by 7404FieldModule.finrank · cited by 1770Module.finrankFintype.card · cited by 1386Fintype.cardModule.finrank_eq_of_rank_eq · cited by 13Module.finrank_eq_of_rank…MvPolynomial.R · cited by 5MvPolynomial.RMvPolynomial.rank_R · cited by 1MvPolynomial.rank_RMvPolynomial.finrank_RCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.