Documentation Verification Report

IsAlgClosed

📁 Source: Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean

Statistics

Metric	Count
Definitions `fieldOfModelACF`, `genericMonicPoly`, `genericMonicPolyHasRoot`, `ACF`	4
Theorems `ACF_categorical`, `ACF_isComplete`, `ACF_isSatisfiable`, `ACF_zero_realize_iff_finite_ACF_prime_not_realize`, `ACF_zero_realize_iff_infinite_ACF_prime_realize`, `finite_ACF_prime_not_realize_of_ACF_zero_realize`, `instModelACFOfCharPOfIsAlgClosed`, `instModelFieldOfCharOfACF`, `isAlgClosed_of_model_ACF`, `lift_genericMonicPoly`, `modelField_of_modelACF`, `realize_genericMonicPolyHasRoot`	12
Total	16

FirstOrder.Field

Definitions

Name	Category	Theorems
`fieldOfModelACF` 📖	CompOp	—
`genericMonicPoly` 📖	CompOp	1 math math: `lift_genericMonicPoly`
`genericMonicPolyHasRoot` 📖	CompOp	1 math math: `realize_genericMonicPolyHasRoot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ACF_categorical` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	`Cardinal.Categorical` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF`	—	`modelField_of_modelACF` `isAlgClosed_of_model_ACF` `charP_of_model_fieldOfChar` `instModelFieldOfCharOfACF` `IsAlgClosed.ringEquiv_of_equiv_of_char_eq` `Cardinal.eq`
`ACF_isComplete` 📖	mathematical	`Nat.Prime`	`FirstOrder.Language.Theory.IsComplete` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF`	—	`Cardinal.Categorical.isComplete` `ACF_categorical` `Order.lt_succ` `Cardinal.instNoMaxOrder` `Order.le_succ` `Nat.instAtLeastTwoHAddOfNat` `FirstOrder.Ring.card_ring` `Cardinal.lift_id'` `le_trans` `le_of_lt` `Cardinal.lt_aleph0_of_finite` `instFiniteULift` `Finite.of_fintype` `ACF_isSatisfiable` `modelField_of_modelACF` `isAlgClosed_of_model_ACF` `IsAlgClosed.instInfinite`
`ACF_isSatisfiable` 📖	mathematical	`Nat.Prime`	`FirstOrder.Language.Theory.IsSatisfiable` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF`	—	`instModelACFOfCharPOfIsAlgClosed` `AlgebraicClosure.instCharP` `ZMod.charP` `AlgebraicClosure.isAlgClosed` `CharP.ofCharZero` `Rat.instCharZero`
`ACF_zero_realize_iff_finite_ACF_prime_not_realize` 📖	mathematical	—	`FirstOrder.Language.Theory.ModelsBoundedFormula` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF` `Set.Finite` `Nat.Primes` `Compl.compl` `Set` `Set.instCompl` `setOf` `Nat.Prime`	—	`finite_ACF_prime_not_realize_of_ACF_zero_realize` `ACF_zero_realize_iff_infinite_ACF_prime_realize` `Set.infinite_of_finite_compl` `Nat.Primes.infinite`
`ACF_zero_realize_iff_infinite_ACF_prime_realize` 📖	mathematical	—	`FirstOrder.Language.Theory.ModelsBoundedFormula` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF` `Set.Infinite` `Nat.Primes` `setOf` `Nat.Prime`	—	`Set.infinite_of_finite_compl` `Nat.Primes.infinite` `finite_ACF_prime_not_realize_of_ACF_zero_realize` `not_imp_not` `FirstOrder.Language.Theory.IsComplete.models_not_iff` `ACF_isComplete`
`finite_ACF_prime_not_realize_of_ACF_zero_realize` 📖	mathematical	`FirstOrder.Language.Theory.ModelsBoundedFormula` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.ACF`	`Set.Finite` `Nat.Primes` `setOf` `Nat.Prime`	—	`FirstOrder.Language.Theory.models_iff_finset_models` `Set.mem_image` `Set.mem_union` `Set.union_right_comm` `FirstOrder.Language.Theory.fieldOfChar.eq_1` `FirstOrder.Language.Theory.ACF.eq_1` `FirstOrder.Language.Theory.models_sentence_of_mem` `Set.mem_union_left` `modelField_of_modelACF` `charP_of_model_fieldOfChar` `instModelFieldOfCharOfACF` `FirstOrder.Language.Term.realize_relabel` `FirstOrder.Ring.realize_termOfFreeCommRing` `map_natCast` `RingHom.instRingHomClass` `FirstOrder.Ring.realize_zero` `CharP.charP_iff_prime_eq_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `CharP.eq` `Set.Finite.subset` `Finset.finite_toSet` `Set.compl_subset_comm` `FirstOrder.Language.Theory.models_of_models_theory`
`instModelACFOfCharPOfIsAlgClosed` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `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` `FirstOrder.Language.Theory.ACF`	—	`FirstOrder.Language.Theory.model_union_iff` `model_fieldOfChar_of_charP` `IsAlgClosed.exists_root` `ne_of_gt` `Polynomial.natDegree_pos_iff_degree_pos`
`instModelFieldOfCharOfACF` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.fieldOfChar`	—	`FirstOrder.Language.Theory.Model.mono` `Set.subset_union_left`
`isAlgClosed_of_model_ACF` 📖	mathematical	—	`IsAlgClosed`	—	`IsAlgClosed.of_exists_root` `FirstOrder.Language.Theory.Model.mono` `Polynomial.natDegree_pos_iff_degree_pos` `Polynomial.degree_pos_of_irreducible` `realize_genericMonicPolyHasRoot`
`lift_genericMonicPoly` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingFreeCommRing` `RingHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeCommRing.lift` `genericMonicPoly` `Polynomial.eval` `Polynomial` `Polynomial.Monic` `Polynomial.natDegree` `Equiv.symm` `Equiv.trans` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Polynomial.degreeLT` `Polynomial.monicEquivDegreeLT` `LinearEquiv.toEquiv` `Submodule.addCommMonoid` `Pi.addCommMonoid` `Submodule.module` `Pi.Function.module` `RingHom.id` `RingHomInvPair.ids` `Polynomial.degreeLTEquiv`	—	`RingHomInvPair.ids` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `FreeCommRing.lift_of` `map_sum` `Finset.sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Polynomial.eval_add` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_finset_sum` `Polynomial.eval_monomial`
`modelField_of_modelACF` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ring` `FirstOrder.Language.Theory.field`	—	`FirstOrder.Language.Theory.Model.mono` `Set.subset_union_of_subset_left` `Set.subset_union_left`
`realize_genericMonicPolyHasRoot` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `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` `genericMonicPolyHasRoot` `Polynomial.eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `Polynomial.Monic` `Polynomial.natDegree`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHomInvPair.ids` `Equiv.forall_congr_left` `Empty.instIsEmpty` `FirstOrder.Language.Term.realize_relabel` `FirstOrder.Ring.realize_termOfFreeCommRing` `lift_genericMonicPoly` `Fin.snoc_last` `Fin.snoc_comp_castSucc` `FirstOrder.Ring.realize_zero`

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`ACF` 📖	CompOp	8 math math: `FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime`, `FirstOrder.Field.ACF_categorical`, `FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize`, `FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero`, `FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed`, `FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize`, `FirstOrder.Field.ACF_isSatisfiable`, `FirstOrder.Field.ACF_isComplete`

---

← Back to Index