Theorems · Inductive type · ring theory

Algebra.IsCentral

(K : Type u) → [inst : CommSemiring K] → (D : Type v) → [inst_1 : Semiring D] → [Algebra K D] → Prop

For a commutative ring K and a K-algebra D, we say that D is a central algebra over K if the center of D is the image of K in D.

Defined in

Mathlib.Algebra.Central.Defs

Cited by

17 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebra