Theorems · Inductive type · commutative algebra

IsAdjoinRoot

{R : Type u} →
  (S : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring S] → [Algebra R S] → Polynomial R → Type (max u v)

IsAdjoinRoot S f states that the ring S can be constructed by adjoining a specified root of the polynomial f : R[X] to R. Compare PowerBasis R S, which does not explicitly specify which polynomial we adjoin a root of (in particular f does not need to be the minimal polynomial of the root we adjoin), and AdjoinRoot which constructs a new type. This is not a typeclass because the choice of root given S and f is not unique.

Defined in

Mathlib.RingTheory.IsAdjoinRoot

Cited by

61 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebra