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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero 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	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval MulZeroClass.toZero 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	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval MulZeroClass.toZero 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	Subtype.fintype Fintype.decidableForallFintype DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval MulZeroClass.toZero 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	Subtype.fintype Finset.decidableDforallFinset DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval MulZeroClass.toZero 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 MvPolynomial.totalDegree_pow Finset.mul_sum mul_lt_mul_of_pos_left LinearOrderedCommMonoidWithZero.toPosMulStrictMono

---

← Back to Index