Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-16 17:05 ad8387cc

View on Github →

feat(field_theory/finite): cardinality of images of polynomials (#1554)

feat(field_theory/finite): cardinality of images of polynomials
docstrings
Johan's suggestions
slightly shorten proof

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.card_eq_sum_card_image

added theorem finset.card_le_mul_card_image

Modified src/data/polynomial.lean

added theorem polynomial.card_roots_sub_C'

added theorem polynomial.card_roots_sub_C

added theorem polynomial.degree_add_C

added theorem polynomial.mem_roots_sub_C

added theorem polynomial.nat_degree_neg

Modified src/field_theory/finite.lean

added theorem finite_field.card_image_polynomial_eval

added theorem finite_field.exists_root_sum_quadratic