Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 15:12 2cf5d19e

View on Github →

chore(algebra/*): Fix lint (#16128) Satisfy the fintype_finite and to_additive_doc linters.

Estimated changes

Modified src/algebra/big_operators/fin.lean

Modified src/algebra/big_operators/finprod.lean

modified theorem finprod_mem_Union

Modified src/algebra/big_operators/pi.lean

modified theorem add_monoid_hom.functions_ext'

modified theorem add_monoid_hom.functions_ext

modified theorem ring_hom.functions_ext

Modified src/algebra/category/Group/limits.lean

Modified src/algebra/char_p/basic.lean

modified theorem is_square_of_char_two'

Modified src/algebra/hom/freiman.lean

Modified src/algebra/order/group.lean

Modified src/algebra/order/lattice_group.lean