mathlib3

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

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