Theorems · Theorem · logic and foundations

FirstOrder.Field.lift_genericMonicPoly

∀ {K : Type u_1} [inst : CommRing K] [inst_1 : Nontrivial K] {n : ℕ} (v : Fin (n + 1) → K),
  (FreeCommRing.lift v) (FirstOrder.Field.genericMonicPoly n) =
    Polynomial.eval (v (Fin.last n))
      ↑(((Polynomial.monicEquivDegreeLT n).trans (Polynomial.degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))

Defined in

Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingNontrivial