Theorems · Inductive type · commutative algebra

Algebra.Presentation

(R : Type u) →
  (S : Type v) →
    Type w → Type t → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max (max t u) v) w)

A presentation of an R-algebra S is a family of generators with σ → MvPolynomial ι R: The assignment of each relation to a polynomial in the generators.

Defined in

Mathlib.RingTheory.Extension.Presentation.Basic

Cited by

70 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebra