Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-16 07:09 47a377d2

View on Github →

refactor(group_theory/quotient_group): remove duplicate definition (#259)

Estimated changes

Modified group_theory/coset.lean

deleted theorem left_cosets.coe_gpow

deleted theorem left_cosets.coe_inv

deleted theorem left_cosets.coe_mul

deleted theorem left_cosets.coe_one

deleted theorem left_cosets.coe_pow

deleted theorem left_cosets.eq_class_eq_left_coset

deleted def left_cosets.mk

deleted def left_cosets

deleted def left_rel

added theorem quotient_group.eq_class_eq_left_coset

added def quotient_group.left_rel

added def quotient_group.mk

added def quotient_group.quotient

Modified group_theory/group_action.lean

modified theorem is_group_action.orbit_eq_iff

Modified group_theory/order_of_element.lean

Modified group_theory/quotient_group.lean

deleted theorem group.quotient.injective_ker_lift

deleted def group.quotient.lift

deleted theorem group.quotient.lift_mk'

deleted theorem group.quotient.lift_mk

deleted def group.quotient.mk

added theorem quotient_group.coe_gpow

added theorem quotient_group.coe_inv

added theorem quotient_group.coe_mul

added theorem quotient_group.coe_one

added theorem quotient_group.coe_pow

added theorem quotient_group.injective_ker_lift

added def quotient_group.lift

added theorem quotient_group.lift_mk'

added theorem quotient_group.lift_mk

Modified group_theory/subgroup.lean

added theorem normal_subgroup_of_comm_group