Theorems · Theorem · commutative algebra

HenselianLocalRing.TFAE

∀ (R : Type u) [inst : CommRing R] [inst_1 : IsLocalRing R],
  [HenselianLocalRing R,
      ∀ (f : Polynomial R),
        f.Monic →
          ∀ (a₀ : IsLocalRing.ResidueField R),
            (Polynomial.aeval a₀) f = 0 →
              (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (IsLocalRing.residue R) a = a₀,
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Function.Surjective ⇑φ →
          ∀ (f : Polynomial R),
            f.Monic →
              ∀ (a₀ : K),
                Polynomial.eval₂ φ a₀ f = 0 →
                  Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE

Defined in

Mathlib.RingTheory.Henselian

Cited by

0 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsLocalRing