Theorems · Inductive type · commutative algebra

PowerBasis

(R : Type u_7) → (S : Type u_8) → [inst : CommRing R] → [inst_1 : Ring S] → [Algebra R S] → Type (max u_7 u_8)

pb : PowerBasis R S states that 1, pb.gen, ..., pb.gen ^ (pb.dim - 1) is a basis for the R-algebra S (viewed as R-module). This is a structure, not a class, since the same algebra can have many power bases. For the common case where S is defined by adjoining an integral element to R, the canonical power basis is given by {Algebra,IntermediateField}.adjoin.powerBasis.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

115 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 21 definitions · uses no axioms

Assumes

CommRingRingAlgebra