Structures · Algebra

HenselianLocalRing

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

Shape

One type argument · adds is_henselian