Theorems · Inductive type · commutative algebra

Algebra.IsGeometricallyReduced

(R : Type u_3) → (A : Type u_4) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop

An R-algebra A is geometrically reduced iff for every prime ideal p of R the base change to AlgebraicClosure p.ResidueField` is reduced.

Defined in

Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Cited by

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingRingAlgebra