Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-05 19:08 a66d0a81

View on Github →

chore(field_theory/finite): meaningful variable names (#2606)

Estimated changes

Modified src/field_theory/finite.lean

modified theorem card_nth_roots_subgroup_units

modified theorem finite_field.card_image_polynomial_eval

modified theorem finite_field.card_units

modified theorem finite_field.exists_root_sum_quadratic

modified def finite_field.field_of_integral_domain

modified theorem finite_field.pow_card_sub_one_eq_one