Theorems · Inductive type · commutative algebra

HenselianLocalRing

(R : Type u_1) → [CommRing R] → Prop

A local ring R is Henselian if the following condition holds: for every polynomial f over R, with a simple root a₀ over the residue field, there exists a lift a : R of a₀ that is a root of f. (Recall that a root b of a polynomial g is simple if it is not a double root, so if g.derivative.eval b ≠ 0.) In other words, R is local Henselian if it is Henselian at the ideal I, in the sense of HenselianRing.

Defined in

Mathlib.RingTheory.Henselian

Cited by

2 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CommRing