Commit 2021-04-18 18:41 30ee691e

View on Github →

feat(group_theory/submonoid/operations): add lemmas (#7219) Some lemmas about the interaction between additive and multiplicative submonoids. I provided the two version (from additive to multiplicative and the other way), I am not sure if @[to_additive] can automatize this.

Estimated changes

Modified src/group_theory/submonoid/operations.lean

added theorem add_submonoid.of_submonoid_coe

added theorem add_submonoid.of_submonoid_mono

added def add_submonoid.submonoid_equiv

added theorem add_submonoid.submonoid_equiv_coe

added theorem add_submonoid.submonoid_equiv_symm_coe

added theorem add_submonoid.to_submonoid_closure

added theorem add_submonoid.to_submonoid_coe

added theorem add_submonoid.to_submonoid_mono

added theorem submonoid.add_submonoid_equiv_coe

added theorem submonoid.add_submonoid_equiv_symm_coe

added theorem submonoid.of_add_submonoid_coe

added theorem submonoid.of_add_submonoid_mono

added theorem submonoid.to_add_submonoid_closure

added theorem submonoid.to_add_submonoid_coe

added theorem submonoid.to_add_submonoid_mono