ChevalleyWarning

📁 Source: Mathlib/FieldTheory/ChevalleyWarning.lean

Statistics

Metric	Count
Definitions	0
Theorems sum_eval_eq_zero, char_dvd_card_solutions, char_dvd_card_solutions_of_add_lt, char_dvd_card_solutions_of_fintype_sum_lt, char_dvd_card_solutions_of_sum_lt	5
Total	5

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_eval_eq_zero 📖	mathematical	totalDegree Semifield.toCommSemiring Field.toSemifield Fintype.card	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.univ Pi.instFintype DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr eval_eq' Finset.sum_comm Finset.sum_eq_zero exists_degree_lt Finset.mul_sum mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain Fintype.sum_fiberwise Fintype.sum_eq_zero Equiv.sum_comp Fintype.sum_congr Equiv.prod_comp Fintype.prod_sum_type Subtype.val_injective Finset.univ_unique Finset.prod_singleton Equiv.subtypeEquivCodomain_symm_apply_eq Fintype.prod_congr Equiv.subtypeEquivCodomain_symm_apply_ne mul_comm FiniteField.sum_pow_lt_card_sub_one MulZeroClass.mul_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
char_dvd_card_solutions 📖	mathematical	MvPolynomial.totalDegree Semifield.toCommSemiring Field.toSemifield Fintype.card	Fintype.card DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subtype.fintype Pi.instFintype	—	Fintype.card_congr' Finset.univ_unique char_dvd_card_solutions_of_sum_lt
char_dvd_card_solutions_of_add_lt 📖	mathematical	MvPolynomial.totalDegree Semifield.toCommSemiring Field.toSemifield Fintype.card	Fintype.card DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subtype.fintype Pi.instFintype	—	Eq.trans_lt add_comm Fintype.card_congr' char_dvd_card_solutions_of_fintype_sum_lt
char_dvd_card_solutions_of_fintype_sum_lt 📖	mathematical	Finset.sum Nat.instAddCommMonoid Finset.univ MvPolynomial.totalDegree Semifield.toCommSemiring Field.toSemifield Fintype.card	Fintype.card Subtype.fintype Fintype.decidableForallFintype DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.instFintype	—	Fintype.card_congr' char_dvd_card_solutions_of_sum_lt
char_dvd_card_solutions_of_sum_lt 📖	mathematical	Finset.sum Nat.instAddCommMonoid MvPolynomial.totalDegree Semifield.toCommSemiring Field.toSemifield Fintype.card	Fintype.card Subtype.fintype Finset.decidableDforallFinset DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.instFintype	—	Fintype.card_units Fintype.card_pos_iff MvPolynomial.eval_prod Finset.prod_congr RingHom.map_sub RingHom.map_one RingHom.map_pow Finset.prod_eq_one zero_pow LT.lt.ne' sub_zero Finset.prod_eq_zero FiniteField.pow_card_sub_one_eq_one sub_self Fintype.card_of_subtype Finset.card_eq_sum_ones Nat.cast_sum Nat.cast_one Fintype.sum_extend_by_zero Finset.sum_congr CharP.cast_eq_zero_iff MvPolynomial.sum_eval_eq_zero MvPolynomial.totalDegree_finset_prod Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid MvPolynomial.totalDegree_sub MvPolynomial.totalDegree_one sup_of_le_right Nat.instCanonicallyOrderedAdd instReflLe MvPolynomial.totalDegree_pow Finset.mul_sum mul_lt_mul_of_pos_left LinearOrderedCommMonoidWithZero.toPosMulStrictMono

---

← Back to Index