Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-17 20:01 cdf97dcc

View on Github →

refactor(field_theory): preparations for Chevalley–Warning (#2590) This PR adds some preparations for the Chevalley–Warning theorem. depends on: ~~#2606, #2607, #2623~~

Estimated changes

Modified src/algebra/group/units.lean

added theorem units.coe_val_hom

added def units.val_hom

Modified src/field_theory/finite.lean

modified theorem finite_field.card'

modified theorem finite_field.card

modified theorem finite_field.card_image_polynomial_eval

added theorem finite_field.cast_card_eq_zero

modified theorem finite_field.exists_root_sum_quadratic

deleted def finite_field.field_of_integral_domain

added theorem finite_field.forall_pow_eq_one_iff

modified theorem finite_field.pow_card_sub_one_eq_one

added theorem finite_field.sum_pow_lt_card_sub_one

added theorem finite_field.sum_pow_units

Modified src/ring_theory/integral_domain.lean

modified theorem card_fiber_eq_of_mem_range

modified theorem card_nth_roots_subgroup_units

added def field_of_integral_domain

added theorem is_cyclic_of_subgroup_integral_domain