Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-11 17:46 98ece77e

View on Github →

refactor(algebra/group): split into smaller files (#1121)

  • rename src/algebra/group.lean → src/algebra/group/default.lean
  • Split algebra/group/default into smaller files No code changes, except for variables declaration and imports
  • Fix compile
  • fix compile error: import anti_hom in algebra/group/default
  • Drop unused imports

Estimated changes

deleted theorem add_add_sub_cancel
deleted theorem add_sub_cancel'
deleted theorem add_sub_cancel'_right
deleted theorem add_sub_sub_cancel
deleted def additive
deleted theorem bit0_zero
deleted theorem bit1_zero
deleted theorem conj_inv
deleted theorem conj_mul
deleted def divp
deleted theorem divp_assoc
deleted theorem divp_eq_one
deleted theorem divp_mul_cancel
deleted theorem divp_one
deleted theorem divp_right_inj
deleted theorem divp_self
deleted theorem eq_iff_eq_of_sub_eq_sub
deleted theorem eq_inv_iff_eq_inv
deleted theorem eq_inv_iff_mul_eq_one
deleted theorem eq_inv_mul_iff_mul_eq
deleted theorem eq_mul_inv_iff_mul_eq
deleted theorem eq_of_inv_eq_inv
deleted theorem eq_sub_iff_add_eq'
deleted theorem eq_sub_iff_add_eq
deleted theorem free_add_monoid.add_def
deleted theorem free_add_monoid.zero_def
deleted def free_add_monoid
deleted theorem free_monoid.mul_def
deleted theorem free_monoid.one_def
deleted def free_monoid
deleted theorem inv.is_group_hom
deleted theorem inv_comm_of_comm
deleted theorem inv_eq_iff_inv_eq
deleted theorem inv_eq_iff_mul_eq_one
deleted theorem inv_eq_one
deleted theorem inv_inj'
deleted theorem inv_is_group_anti_hom
deleted theorem inv_mul_eq_iff_eq_mul
deleted theorem inv_ne_one
deleted theorem is_add_group_hom.map_sub
deleted theorem is_add_group_hom.sub
deleted theorem is_add_monoid_hom.map_add
deleted def is_conj
deleted theorem is_conj_iff_eq
deleted theorem is_conj_one_left
deleted theorem is_conj_one_right
deleted theorem is_conj_refl
deleted theorem is_conj_symm
deleted theorem is_conj_trans
deleted theorem is_group_anti_hom.map_inv
deleted theorem is_group_anti_hom.map_one
deleted theorem is_group_hom.inv
deleted theorem is_group_hom.map_inv
deleted theorem is_group_hom.map_one
deleted theorem is_group_hom.mul
deleted theorem is_monoid_hom.map_mul
deleted theorem is_mul_hom.comp'
deleted theorem is_mul_hom.comp
deleted theorem is_mul_hom.id
deleted theorem left_inverse_add_left_sub
deleted theorem left_inverse_inv
deleted theorem left_inverse_sub_add_left
deleted theorem mul_divp_cancel
deleted theorem mul_eq_one_iff_eq_inv
deleted theorem mul_eq_one_iff_inv_eq
deleted theorem mul_inv_eq_iff_eq_mul
deleted theorem mul_inv_eq_one
deleted theorem mul_left_inj
deleted theorem mul_mul_mul_comm
deleted theorem mul_right_inj
deleted theorem mul_self_iff_eq_one
deleted def multiplicative
deleted theorem nat.units_eq_one
deleted theorem neg_add'
deleted theorem neg_sub_neg
deleted theorem one_divp
deleted theorem sub_add_add_cancel
deleted theorem sub_add_sub_cancel'
deleted theorem sub_add_sub_cancel
deleted theorem sub_eq_iff_eq_add'
deleted theorem sub_eq_iff_eq_add
deleted theorem sub_eq_neg_add
deleted theorem sub_eq_sub_iff_sub_eq_sub
deleted theorem sub_eq_zero
deleted theorem sub_left_inj
deleted theorem sub_ne_zero
deleted theorem sub_right_comm
deleted theorem sub_right_inj
deleted def sub_sub_cancel
deleted theorem sub_sub_sub_cancel_left
deleted theorem sub_sub_sub_cancel_right
deleted theorem units.coe_inv
deleted theorem units.coe_map
deleted theorem units.coe_mul
deleted theorem units.coe_one
deleted theorem units.ext
deleted theorem units.ext_iff
deleted theorem units.inv_mul
deleted theorem units.inv_mul_cancel_left
deleted theorem units.map_comp'
deleted theorem units.map_comp
deleted theorem units.map_id
deleted theorem units.mul_inv
deleted theorem units.mul_inv_cancel_left
deleted theorem units.mul_left_inj
deleted theorem units.mul_right_inj
deleted theorem units.val_coe
deleted structure units
deleted theorem with_one.coe_inj
deleted theorem with_one.coe_ne_one
deleted theorem with_one.mul_coe
deleted theorem with_one.one_ne_coe
deleted def with_one
deleted theorem with_zero.coe_one
deleted theorem with_zero.div_coe
deleted theorem with_zero.div_eq_div
deleted theorem with_zero.div_mul_cancel
deleted theorem with_zero.div_one
deleted theorem with_zero.div_zero
deleted theorem with_zero.inv_coe
deleted theorem with_zero.inv_one
deleted theorem with_zero.inv_zero
deleted theorem with_zero.mul_coe
deleted theorem with_zero.mul_div_cancel
deleted theorem with_zero.mul_inv_rev
deleted theorem with_zero.mul_left_inv
deleted theorem with_zero.mul_right_inv
deleted theorem with_zero.one_div
deleted theorem with_zero.zero_div
added theorem inv_is_group_anti_hom
added theorem add_add_sub_cancel
added theorem add_sub_cancel'
added theorem add_sub_cancel'_right
added theorem add_sub_sub_cancel
added theorem bit0_zero
added theorem bit1_zero
added theorem eq_inv_iff_eq_inv
added theorem eq_inv_iff_mul_eq_one
added theorem eq_inv_mul_iff_mul_eq
added theorem eq_mul_inv_iff_mul_eq
added theorem eq_of_inv_eq_inv
added theorem eq_sub_iff_add_eq'
added theorem eq_sub_iff_add_eq
added theorem inv_comm_of_comm
added theorem inv_eq_iff_inv_eq
added theorem inv_eq_iff_mul_eq_one
added theorem inv_eq_one
added theorem inv_inj'
added theorem inv_mul_eq_iff_eq_mul
added theorem inv_ne_one
added theorem left_inverse_inv
added theorem mul_eq_one_iff_eq_inv
added theorem mul_eq_one_iff_inv_eq
added theorem mul_inv_eq_iff_eq_mul
added theorem mul_inv_eq_one
added theorem mul_left_inj
added theorem mul_mul_mul_comm
added theorem mul_right_inj
added theorem mul_self_iff_eq_one
added theorem neg_add'
added theorem neg_sub_neg
added theorem sub_add_add_cancel
added theorem sub_add_sub_cancel'
added theorem sub_add_sub_cancel
added theorem sub_eq_iff_eq_add'
added theorem sub_eq_iff_eq_add
added theorem sub_eq_neg_add
added theorem sub_eq_zero
added theorem sub_left_inj
added theorem sub_ne_zero
added theorem sub_right_comm
added theorem sub_right_inj
added def sub_sub_cancel
added theorem conj_inv
added theorem conj_mul
added def is_conj
added theorem is_conj_iff_eq
added theorem is_conj_one_left
added theorem is_conj_one_right
added theorem is_conj_refl
added theorem is_conj_symm
added theorem is_conj_trans
added def free_add_monoid
added theorem free_monoid.mul_def
added theorem free_monoid.one_def
added def free_monoid
added theorem inv.is_group_hom
added theorem is_add_group_hom.sub
added theorem is_group_hom.inv
added theorem is_group_hom.map_inv
added theorem is_group_hom.map_one
added theorem is_group_hom.mul
added theorem is_monoid_hom.map_mul
added theorem is_mul_hom.comp'
added theorem is_mul_hom.comp
added theorem is_mul_hom.id
added def additive
added def multiplicative
added def divp
added theorem divp_assoc
added theorem divp_eq_one
added theorem divp_mul_cancel
added theorem divp_one
added theorem divp_right_inj
added theorem divp_self
added theorem mul_divp_cancel
added theorem nat.units_eq_one
added theorem one_divp
added theorem units.coe_inv
added theorem units.coe_mul
added theorem units.coe_one
added theorem units.ext
added theorem units.ext_iff
added theorem units.inv_mul
added theorem units.mul_inv
added theorem units.mul_left_inj
added theorem units.mul_right_inj
added theorem units.val_coe
added structure units
added theorem units.coe_map
added theorem units.map_comp'
added theorem units.map_comp
added theorem units.map_id
added theorem with_one.coe_inj
added theorem with_one.coe_ne_one
added theorem with_one.mul_coe
added theorem with_one.one_ne_coe
added def with_one
added theorem with_zero.coe_one
added theorem with_zero.div_coe
added theorem with_zero.div_eq_div
added theorem with_zero.div_one
added theorem with_zero.div_zero
added theorem with_zero.inv_coe
added theorem with_zero.inv_one
added theorem with_zero.inv_zero
added theorem with_zero.mul_coe
added theorem with_zero.mul_inv_rev
added theorem with_zero.mul_left_inv
added theorem with_zero.one_div
added theorem with_zero.zero_div