Mathlib Map

Theorems · Definition · commutative algebra

PowerBasis.dim

{R : Type u_7} → {S : Type u_8} → [inst : CommRing R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → PowerBasis R S → ℕ
Defined in
Mathlib.RingTheory.PowerBasis
Cited by
74 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
CommRingRingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PowerBasis.basis · cited by 54PowerBasis.basisPowerBasis.finrank · cited by 14PowerBasis.finrankIntermediateField.adjoin.finrank · cited by 14adjoin.finrankPowerBasis.basis_eq_pow · cited by 13PowerBasis.basis_eq_powPowerBasis.coe_basis · cited by 12PowerBasis.coe_basisPowerBasis.lift · cited by 9PowerBasis.liftPowerBasis.minpolyGen · cited by 9PowerBasis.minpolyGenPowerBasis.natDegree_minpoly · cited by 8PowerBasis.natDegree_minp…PowerBasis.map · cited by 7PowerBasis.mapPowerBasis.dim_pos · cited by 5PowerBasis.dim_posAlgebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly · cited by 5PowerBasis.norm_gen_eq_co…PowerBasis.adjoin_gen_eq_top · cited by 4PowerBasis.adjoin_gen_eq_…PowerBasis.constr_pow_aeval · cited by 4PowerBasis.constr_pow_aev…IsCyclotomicExtension.discr_prime_pow_ne_two · cited by 4IsCyclotomicExtension.dis…IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one · cited by 4IsPrimitiveRoot.discr_zet…CommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraRing · cited by 7463RingPowerBasis · cited by 115PowerBasisPowerBasis.dimCITED BYCITES

Cites4

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

  • CommRingstatement and proof · cited by 17,173
  • Algebrastatement and proof · cited by 11,388
  • Ringstatement and proof · cited by 7,463
  • PowerBasisstatement and proof · cited by 115

Cited by78

Results whose statement or proof uses this declaration.