Theorems · Definition · algebraic geometry

FirstOrder.genericPolyMapSurjOnOfInjOn

{ι : Type u_1} →
  {α : Type u_2} →
    [Finite α] →
      [Finite ι] → FirstOrder.Language.ring.Formula (α ⊕ ι) → (ι → Finset (ι →₀ ℕ)) → FirstOrder.Language.ring.Sentence

The collection of first-order formulas corresponding to the Ax-Grothendieck theorem.

Defined in

Mathlib.FieldTheory.AxGrothendieck

Cited by

4 results in Mathlib

Foundations

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

Assumes

FiniteFinite