Commit 2022-11-13 03:11 f86ad885

View on Github →

move(group_theory/group_action/*): Move pointwise subgroup operations (#17491) ... from group_theory.group_action.basic to group_theory.group_action.pointwise.

Estimated changes

Modified src/algebra/module/linear_map.lean

Modified src/data/dfinsupp/lex.lean

Modified src/group_theory/group_action/basic.lean

Modified src/group_theory/quotient_group.lean

Modified src/group_theory/subgroup/basic.lean

deleted theorem inv_coe_set

deleted theorem subgroup.closure_induction''

deleted theorem subgroup.closure_induction_left

deleted theorem subgroup.closure_induction_right

deleted theorem subgroup.closure_inv

deleted theorem subgroup.closure_mul_le

deleted theorem subgroup.closure_to_submonoid

deleted theorem subgroup.inf_mul_assoc

deleted theorem subgroup.inv_subset_closure

deleted theorem subgroup.mul_inf_assoc

deleted theorem subgroup.mul_normal

deleted theorem subgroup.normal_mul

deleted theorem subgroup.smul_opposite_image_mul_preimage

deleted theorem subgroup.sup_eq_closure

deleted theorem subgroup.supr_induction'

deleted theorem subgroup.supr_induction

Modified src/group_theory/subgroup/pointwise.lean

added theorem inv_coe_set

added theorem subgroup.closure_induction''

added theorem subgroup.closure_induction_left

added theorem subgroup.closure_induction_right

added theorem subgroup.closure_inv

added theorem subgroup.closure_mul_le

added theorem subgroup.closure_to_submonoid

added theorem subgroup.inf_mul_assoc

added theorem subgroup.inv_subset_closure

added theorem subgroup.mul_inf_assoc

added theorem subgroup.mul_normal

added theorem subgroup.normal_mul

added theorem subgroup.smul_opposite_image_mul_preimage

added theorem subgroup.sup_eq_closure

added theorem subgroup.supr_induction'

added theorem subgroup.supr_induction

Modified src/linear_algebra/basic.lean

modified theorem submodule.neg_coe

Modified src/ring_theory/subsemiring/pointwise.lean