Definability

📁 Source: Mathlib/ModelTheory/Algebra/Ring/Definability.lean

Statistics

Metric	Count
Definitions	0
Theorems mvPolynomial_zeroLocus_definable	1
Total	1

FirstOrder.Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mvPolynomial_zeroLocus_definable 📖	mathematical	—	Set.Definable Set.iUnion MvPolynomial Semifield.toCommSemiring Field.toSemifield Finset Finset.instMembership Set.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial.coeff SetLike.coe Finset.instSetLike MvPolynomial.support FirstOrder.Language.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 NonUnitalNonAssocSemiring.toMulZeroClass MvPolynomial.zeroLocus Algebra.id Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring	—	Set.definable_iff_exists_formula_sum MvPolynomial.zeroLocus_span Finite.of_fintype Set.mem_image_of_mem Fin.isEmpty' FirstOrder.Language.BoundedFormula.iInf.congr_simp FirstOrder.Language.Term.relabel_relabel FirstOrder.Language.Term.realize_relabel realize_termOfFreeCommRing lift_genericPolyMap Finset.Subset.refl MvPolynomialSupportLEEquiv_symm_apply_coeff realize_zero

---

← Back to Index