Commit 2021-04-15 20:50 b4201e7b

View on Github →

chore(group/ring_hom): fix a nat nsmul diamond (#7201) The space of additive monoid should be given a proper nat-action, by the pointwise action, to avoid diamonds.

Estimated changes

Modified src/algebra/group/hom.lean

deleted def monoid_hom.comp_hom

deleted def monoid_hom.eval

deleted theorem monoid_hom.eval_apply

deleted def monoid_hom.flip

deleted theorem monoid_hom.flip_apply

deleted def monoid_hom.flip_hom

Created src/algebra/group/hom_instances.lean

added def monoid_hom.comp_hom

added def monoid_hom.eval

added theorem monoid_hom.eval_apply

added def monoid_hom.flip

added theorem monoid_hom.flip_apply

added def monoid_hom.flip_hom

added theorem nat.succ_eq_one_add

Modified src/algebra/group/pi.lean

Modified src/algebra/group_power/basic.lean

Modified src/algebra/module/basic.lean

deleted theorem add_monoid_hom.nat_smul_apply

Modified src/data/nat/basic.lean

deleted theorem nat.succ_eq_one_add