Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-01 07:06 3a0c0345

View on Github →

chore(algebra/*): generalisation linter (#13099)

Estimated changes

Modified src/algebra/group/prod.lean

modified theorem prod.fst_div

modified theorem prod.mk_div_mk

modified theorem prod.snd_div

modified theorem prod.swap_div

Modified src/algebra/hom/group.lean

modified theorem monoid_hom.mul_comp

modified theorem monoid_with_zero_hom.to_monoid_hom_injective

modified theorem monoid_with_zero_hom.to_zero_hom_injective

modified theorem mul_hom.mul_comp

Modified src/algebra/hom/group_instances.lean

modified def monoid_hom.compl₂

modified theorem monoid_hom.compl₂_apply