Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-02 10:49 9556784a

View on Github →

chore(ring_theory/*): Fix lint (#16350) Satisfy the fintype_finite and check_reducibility linters.

Estimated changes

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/ideal/quotient.lean

modified theorem ideal.exists_sub_mem

modified theorem ideal.map_pi

modified theorem ideal.quotient_inf_to_pi_quotient_bijective

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/localization/integer.lean

added theorem is_localization.exist_integer_multiples_of_finite

deleted theorem is_localization.exist_integer_multiples_of_fintype

Modified src/ring_theory/norm.lean

modified theorem algebra.norm_algebra_map_of_basis

modified theorem algebra.norm_eq_matrix_det

Modified src/ring_theory/nullstellensatz.lean

Modified src/ring_theory/polynomial/basic.lean

modified theorem mv_polynomial.map_mv_polynomial_eq_eval₂

Modified src/ring_theory/trace.lean

modified theorem algebra.trace_comp_trace_of_basis

modified theorem algebra.trace_trace_of_basis

Modified src/ring_theory/witt_vector/basic.lean