Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 02:06 543359ce

View on Github →

feat(field_theory/finite): Chevalley–Warning (#1564)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.coe_subtype_equiv_codomain

added theorem equiv.coe_subtype_equiv_codomain_symm

added def equiv.subtype_equiv_codomain

added theorem equiv.subtype_equiv_codomain_apply

added theorem equiv.subtype_equiv_codomain_symm_apply

added theorem equiv.subtype_equiv_codomain_symm_apply_eq

added theorem equiv.subtype_equiv_codomain_symm_apply_ne

Modified src/data/finsupp.lean

added theorem finsupp.prod_fintype

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.eval_eq'

added theorem mv_polynomial.eval_eq

added theorem mv_polynomial.eval_prod

added theorem mv_polynomial.eval_sum

added theorem mv_polynomial.eval₂_eq'

added theorem mv_polynomial.eval₂_eq

added theorem mv_polynomial.exists_degree_lt

Created src/field_theory/chevalley_warning.lean

added theorem char_dvd_card_solutions

added theorem char_dvd_card_solutions_family

added theorem mv_polynomial.sum_mv_polynomial_eq_zero