Mathlib Map

Theorems · Definition · commutative algebra

PowerBasis.gen

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

Around this declaration

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

PowerBasis.basis_eq_pow · cited by 13PowerBasis.basis_eq_powPowerBasis.coe_basis · cited by 12PowerBasis.coe_basisIntermediateField.adjoin.powerBasis_gen · cited by 10adjoin.powerBasis_genPowerBasis.lift · cited by 9PowerBasis.liftPowerBasis.minpolyGen · cited by 9PowerBasis.minpolyGenAdjoinRoot.equiv' · cited by 9AdjoinRoot.equiv'PowerBasis.equivOfMinpoly · cited by 8PowerBasis.equivOfMinpolyPowerBasis.natDegree_minpoly · cited by 8PowerBasis.natDegree_minp…IsPrimitiveRoot.powerBasis_gen · cited by 8IsPrimitiveRoot.powerBasi…PowerBasis.map · cited by 7PowerBasis.mapPowerBasis.map_gen · cited by 7PowerBasis.map_genPowerBasis.equivOfRoot · cited by 6PowerBasis.equivOfRootAlgebra.adjoin.powerBasis'_gen · cited by 5adjoin.powerBasis'_genPowerBasis.liftEquiv' · cited by 5PowerBasis.liftEquiv'PowerBasis.quotientEquivQuotientMinpolyMap · cited by 5PowerBasis.quotientEquivQ…CommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraRing · cited by 7463RingPowerBasis · cited by 115PowerBasisPowerBasis.genCITED 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 by134

Results whose statement or proof uses this declaration.