Commit 2023-02-01 11:22 b746237a

View on Github →

feat: port GroupTheory.Subgroup.Pointwise (#1981)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Created Mathlib/GroupTheory/Subgroup/Pointwise.lean

added theorem AddSubgroup.coe_pointwise_smul

added theorem AddSubgroup.le_pointwise_smul_iff

added theorem AddSubgroup.le_pointwise_smul_iff₀

added theorem AddSubgroup.mem_inv_pointwise_smul_iff

added theorem AddSubgroup.mem_inv_pointwise_smul_iff₀

added theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem

added theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem AddSubgroup.mem_smul_pointwise_iff_exists

added theorem AddSubgroup.pointwise_smul_le_iff

added theorem AddSubgroup.pointwise_smul_le_iff₀

added theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff

added theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀

added theorem AddSubgroup.pointwise_smul_toAddSubmonoid

added theorem AddSubgroup.smul_mem_pointwise_smul

added theorem AddSubgroup.smul_mem_pointwise_smul_iff

added theorem AddSubgroup.smul_mem_pointwise_smul_iff₀

added theorem Subgroup.Normal.conjAct

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_toSubmonoid

added theorem Subgroup.coe_pointwise_smul

added theorem Subgroup.conj_smul_le_of_le

added theorem Subgroup.conj_smul_subgroupOf

added def Subgroup.equivSmul

added theorem Subgroup.inf_mul_assoc

added theorem Subgroup.inv_subset_closure

added theorem Subgroup.le_pointwise_smul_iff₀

added theorem Subgroup.mem_inv_pointwise_smul_iff

added theorem Subgroup.mem_inv_pointwise_smul_iff₀

added theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem

added theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem Subgroup.mem_smul_pointwise_iff_exists

added theorem Subgroup.mul_inf_assoc

added theorem Subgroup.mul_normal

added theorem Subgroup.normal_mul

added theorem Subgroup.pointwise_smul_def

added theorem Subgroup.pointwise_smul_le_iff₀

added theorem Subgroup.pointwise_smul_le_pointwise_smul_iff

added theorem Subgroup.pointwise_smul_le_pointwise_smul_iff₀

added theorem Subgroup.pointwise_smul_subset_iff

added theorem Subgroup.pointwise_smul_toSubmonoid

added theorem Subgroup.set_mul_normal_comm

added theorem Subgroup.singleton_mul_subgroup

added theorem Subgroup.smul_bot

added theorem Subgroup.smul_closure

added theorem Subgroup.smul_inf

added theorem Subgroup.smul_mem_pointwise_smul

added theorem Subgroup.smul_mem_pointwise_smul_iff

added theorem Subgroup.smul_mem_pointwise_smul_iff₀

added theorem Subgroup.smul_normal

added theorem Subgroup.smul_opposite_image_mul_preimage'

added theorem Subgroup.smul_opposite_image_mul_preimage

added theorem Subgroup.smul_sup

added theorem Subgroup.subgroup_mul_singleton

added theorem Subgroup.subset_pointwise_smul_iff

added theorem Subgroup.sup_eq_closure

added theorem Subgroup.supᵢ_induction'

added theorem Subgroup.supᵢ_induction

added theorem inv_coe_set