Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-20 11:28 c2c31b52

View on Github →

chore(field_theory/*): Fix lint (#16149) Satisfy the fintype_finite linter.

Estimated changes

Modified src/data/fintype/basic.lean

Modified src/field_theory/finite/basic.lean

Modified src/field_theory/finite/galois_field.lean

Modified src/field_theory/finite/polynomial.lean

modified theorem mv_polynomial.eq_zero_of_eval_eq_zero

modified theorem mv_polynomial.ker_evalₗ

modified theorem mv_polynomial.range_evalᵢ

Modified src/field_theory/finite/trace.lean

modified theorem finite_field.trace_to_zmod_nondegenerate

Modified src/field_theory/fixed.lean

modified theorem fixed_points.finrank_le_card

modified theorem fixed_points.is_integral

Modified src/field_theory/galois.lean

Modified src/field_theory/primitive_element.lean

added theorem field.exists_primitive_element_of_finite_bot

added theorem field.exists_primitive_element_of_finite_top

deleted theorem field.exists_primitive_element_of_fintype_bot

deleted theorem field.exists_primitive_element_of_fintype_top

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.finite_of_finite