Commit 2022-03-06 11:52 28c902d8

View on Github →

fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single (#12474) so that the simp-normal form really is pi.mul_single. While adjusting related lemmas in group_theory.subgroup.basic, add a few missing to_additive attributes.

Estimated changes

Modified src/algebra/group/pi.lean

added theorem monoid_hom.single_apply

added theorem one_hom.single_apply

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.mul_single_mem_pi

added theorem subgroup.pi_mem_of_mul_single_mem

added theorem subgroup.pi_mem_of_mul_single_mem_aux

deleted theorem subgroup.pi_mem_of_single_mem

deleted theorem subgroup.pi_mem_of_single_mem_aux

deleted theorem subgroup.single_mem_pi