Theorems · Inductive type · commutative algebra

Algebra.FinitePresentation

(R : Type w₁) → (A : Type w₂) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop

An algebra over a commutative semiring is Algebra.FinitePresentation if it is the quotient of a polynomial ring in n variables by a finitely generated ideal.

Defined in

Mathlib.RingTheory.FinitePresentation

Cited by

56 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebra