Documentation Verification Report

AxGrothendieck

📁 Source: Mathlib/FieldTheory/AxGrothendieck.lean

Statistics

Metric	Count
Definitions `genericPolyMapSurjOnOfInjOn`	1
Theorems `ACF_models_genericPolyMapSurjOnOfInjOn_of_prime`, `ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero`, `realize_genericPolyMapSurjOnOfInjOn`, `ax_grothendieck_of_definable`, `ax_grothendieck_of_locally_finite`, `ax_grothendieck_univ`, `ax_grothendieck_zeroLocus`	7
Total	8

FirstOrder

Definitions

Name	Category	Theorems
`genericPolyMapSurjOnOfInjOn` 📖	CompOp	3 math math: `ACF_models_genericPolyMapSurjOnOfInjOn_of_prime`, `ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero`, `realize_genericPolyMapSurjOnOfInjOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ACF_models_genericPolyMapSurjOnOfInjOn_of_prime` 📖	mathematical	`Nat.Prime`	`Language.Theory.ModelsBoundedFormula` `Language.ring` `Language.Theory.ACF` `genericPolyMapSurjOnOfInjOn`	—	`Language.Theory.IsComplete.realize_sentence_iff` `Field.ACF_isComplete` `Field.instModelACFOfCharPOfIsAlgClosed` `AlgebraicClosure.instCharP` `ZMod.charP` `AlgebraicClosure.isAlgClosed` `realize_genericPolyMapSurjOnOfInjOn` `ax_grothendieck_of_locally_finite` `Finite.of_fintype` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `AlgebraicClosure.isAlgebraic`
`ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero` 📖	mathematical	`Nat.Prime`	`Language.Theory.ModelsBoundedFormula` `Language.ring` `Language.Theory.ACF` `genericPolyMapSurjOnOfInjOn`	—	`ACF_models_genericPolyMapSurjOnOfInjOn_of_prime` `Field.ACF_zero_realize_iff_infinite_ACF_prime_realize` `Set.eq_univ_iff_forall` `Set.infinite_univ` `Nat.Primes.infinite`
`realize_genericPolyMapSurjOnOfInjOn` 📖	mathematical	—	`Language.Sentence.Realize` `Language.ring` `Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `genericPolyMapSurjOnOfInjOn` `Set.SurjOn` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `setOf` `Language.Formula.Realize`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `Language.Term.realize_relabel` `Equiv.forall_congr_left` `Ring.realize_termOfFreeCommRing` `Ring.lift_genericPolyMap` `Fin.cons_zero` `Fin.cons_one` `Fin.instNeZeroHAddNatOfNat_mathlib_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ax_grothendieck_of_definable` 📖	mathematical	`Set.Definable` `FirstOrder.Language.ring` `FirstOrder.Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Set.MapsTo` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Set.InjOn`	`Set.SurjOn`	—	`Set.definable_iff_finitely_definable` `Set.definable_iff_exists_formula_sum` `Finite.of_fintype` `FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero` `CharP.char_is_prime_or_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ringChar.charP` `FirstOrder.realize_genericPolyMapSurjOnOfInjOn` `FirstOrder.Language.Theory.IsComplete.realize_sentence_iff` `FirstOrder.Field.ACF_isComplete` `FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed` `Nontrivial.to_nonempty` `Set.Subset.refl`
`ax_grothendieck_of_locally_finite` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Set.InjOn`	`Set.SurjOn`	—	`isAlgebraic_iff_isIntegral` `Algebra.IsAlgebraic.isAlgebraic` `nonempty_fintype` `Algebra.subset_adjoin` `Finset.mem_union_right` `Finset.mem_image` `Finset.mem_univ` `Finset.mem_union_left` `Finset.mem_biUnion` `Finset.mem_image_of_mem` `isNoetherian_adjoin_finset` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Module.finite_of_finite` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `Module.Projective.of_free` `Module.Free.of_divisionRing` `MvPolynomial.eval_mem` `Subalgebra.instSubsemiringClass` `Finite.injective_iff_surjective` `Subtype.finite` `Pi.finite`
`ax_grothendieck_univ` 📖	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	—	`MvPolynomial.zeroLocus_bot` `ax_grothendieck_zeroLocus`
`ax_grothendieck_zeroLocus` 📖	mathematical	—	`Set.SurjOn` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `MvPolynomial.zeroLocus` `Algebra.id`	—	`IsNoetherian.noetherian` `MvPolynomial.isNoetherianRing` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `ax_grothendieck_of_definable` `FirstOrder.Ring.mvPolynomial_zeroLocus_definable`

---

← Back to Index