Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-10 13:02 88960f08

View on Github →

refactor(algebra): move is_submonoid to group_theory and base is_subgroup on is_submonoid

Estimated changes

Modified algebra/group.lean

modified theorem inv_is_group_anti_hom

modified def is_group_anti_hom

modified def is_group_hom

Modified algebra/group_power.lean

deleted def powers

Modified data/list/basic.lean

Modified group_theory/subgroup.lean

added def gpowers

added theorem injective_mul

modified theorem is_subgroup.cosets_disjoint

added theorem is_subgroup.gpow_mem

deleted theorem is_subgroup.injective_mul

deleted theorem is_subgroup.inv_mem

modified theorem is_subgroup.inv_mem_iff

modified theorem is_subgroup.mul_image

deleted theorem is_subgroup.mul_mem

added theorem is_subgroup.mul_mem_cancel_left

added theorem is_subgroup.mul_mem_cancel_right

added theorem is_subgroup.of_div

modified theorem is_subgroup.subgroup_mem_cosets

deleted structure is_subgroup

deleted theorem is_subgroup_range_gpow

Created group_theory/submonoid.lean

added theorem is_submonoid.pow_mem

added def powers

Modified ring_theory/localization.lean