Theorems · Theorem · field theory

IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C

∀ {k : Type u} [inst : Field k] [IsSepClosed k] {n : ℕ} (a b c : k),
  ↑n = 0 → 2 ≤ n → b ≠ 0 → ∃ x, a * x ^ n + b * x + c = 0

If n ≥ 2 equals zero in a separably closed field k, b ≠ 0, then there exists x in k such that a * x ^ n + b * x + c = 0.

Defined in

Mathlib.FieldTheory.IsSepClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldIsSepClosed