Pointwise

📁 Source: Mathlib/Algebra/Group/Subgroup/Pointwise.lean

Statistics

Metric	Count
Definitions `equivSMul`, `pointwiseMulAction`	2
Theorems `add_inf_assoc`, `add_normal`, `closure_add_le`, `closure_induction''`, `closure_induction_left`, `closure_induction_right`, `closure_neg`, `closure_nsmul`, `closure_nsmul_le`, `closure_singleton_neg`, `closure_toAddSubmonoid`, `coe_add_of_left_le_normalizer_right`, `coe_add_of_right_le_normalizer_left`, `iSup_induction`, `iSup_induction'`, `inf_add_assoc`, `neg_subset_closure`, `normal_add`, `set_add_normal_comm`, `set_add_normalizer_comm`, `sup_eq_closure_add`, `sup_normal`, `toAddSubmonoid_zmultiples`, `vadd_mem_of_mem_closure_of_mem`, `vadd_opposite_image_add_preimage`, `vadd_opposite_image_add_preimage'`, `multiples_le_zmultiples`, `addSubgroupClosure_add`, `addSubgroupClosure_add_nsmul`, `add_addSubgroupClosure`, `mul_subgroupClosure`, `nsmul_add_addSubgroupClosure`, `pow_mul_subgroupClosure`, `subgroupClosure_mul`, `subgroupClosure_mul_pow`, `conjAct`, `conj_smul_eq_self`, `of_conjugate_fixed`, `closure_induction''`, `closure_induction_left`, `closure_induction_right`, `closure_inv`, `closure_mul_le`, `closure_pow`, `closure_pow_le`, `closure_singleton_inv`, `closure_toSubmonoid`, `coe_mul_of_left_le_normalizer_right`, `coe_mul_of_right_le_normalizer_left`, `coe_pointwise_smul`, `conjAct_pointwise_smul_eq_self`, `conjAct_pointwise_smul_iff`, `conj_smul_eq_self_of_mem`, `conj_smul_le_of_le`, `conj_smul_subgroupOf`, `equivSMul_apply_coe`, `equivSMul_symm_apply_coe`, `iSup_induction`, `iSup_induction'`, `inf_mul_assoc`, `instCovariantClassHSMulLe`, `inv_subset_closure`, `mem_inv_pointwise_smul_iff`, `mem_pointwise_smul_iff_inv_smul_mem`, `mem_smul_pointwise_iff_exists`, `mul_inf_assoc`, `mul_normal`, `normalCore_eq_iInf_conjAct`, `normal_mul`, `pointwise_isCentralScalar`, `pointwise_smul_def`, `pointwise_smul_le_pointwise_smul_iff`, `pointwise_smul_subset_iff`, `pointwise_smul_toSubmonoid`, `set_mul_normal_comm`, `set_mul_normalizer_comm`, `singleton_mul_subgroup`, `smul_bot`, `smul_closure`, `smul_inf`, `smul_mem_of_mem_closure_of_mem`, `smul_mem_pointwise_smul`, `smul_mem_pointwise_smul_iff`, `smul_opposite_image_mul_preimage`, `smul_opposite_image_mul_preimage'`, `smul_sup`, `subgroup_mul_singleton`, `subset_pointwise_smul_iff`, `sup_eq_closure_mul`, `sup_normal`, `toSubmonoid_zpowers`, `powers_le_zpowers`, `coe_div_coe`, `coe_set_eq_one`, `coe_set_eq_zero`, `coe_sub_coe`, `inv_coe_set`, `neg_coe_set`, `op_smul_coe_set`, `op_vadd_coe_set`, `smul_coe_set`, `vadd_coe_set`	102
Total	104

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_inf_assoc` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `instSetLike` `instMin` `Set.instInter`	—	`Set.ext` `Set.mem_add` `Set.mem_inter_iff` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `SetLike.mem_coe` `neg_add_cancel_left`
`add_normal` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`coe_add_of_left_le_normalizer_right` `le_normalizer_of_normal`
`closure_add_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`sInf_le` `add_mem` `SetLike.le_def` `instIsConcreteLE` `le_sup_left` `subset_closure` `le_sup_right`
`closure_induction''` 📖	—	`subset_closure` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegMemClass.neg_mem` `AddSubgroup` `instSetLike` `AddSubgroupClass.toNegMemClass` `AddGroup.toSubNegMonoid` `instAddSubgroupClass` `closure` `NegZeroClass.toZero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SetLike.instMembership`	—	—	`subset_closure` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `closure_induction_left`
`closure_induction_left` 📖	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `ZeroMemClass.zero_mem` `AddSubgroup` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `closure` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `subset_closure` `NegZeroClass.toNeg` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `SetLike.instMembership`	—	—	`ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `subset_closure` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `mem_toAddSubmonoid` `closure_toAddSubmonoid` `AddSubmonoid.closure_induction_left` `AddSubmonoid.instAddSubmonoidClass` `AddSubmonoid.subset_closure` `neg_neg`
`closure_induction_right` 📖	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `ZeroMemClass.zero_mem` `AddSubgroup` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `closure` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `subset_closure` `NegZeroClass.toNeg` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `SetLike.instMembership`	—	—	`ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `subset_closure` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `closure_induction_left` `op_closure`
`closure_neg` 📖	mathematical	—	`closure` `Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`closure_toAddSubmonoid` `neg_neg` `Set.union_comm`
`closure_nsmul` 📖	mathematical	`Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`closure` `Set.NSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`LE.le.antisymm` `closure_nsmul_le` `closure_mono` `Set.subset_nsmul`
`closure_nsmul_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `AddMonoid.toNatSMul` `Set.addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`zero_nsmul` `closure_le` `Set.zero_subset` `SetLike.mem_coe` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `succ_nsmul` `le_imp_le_of_le_of_le` `closure_add_le` `le_refl` `sup_le_sup` `sup_idem`
`closure_singleton_neg` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.neg_singleton` `closure_neg`
`closure_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `closure` `AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set` `Set.instUnion` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`le_antisymm` `closure_induction` `AddSubmonoid.closure_mono` `Set.subset_union_left` `AddSubmonoid.subset_closure` `AddSubmonoid.zero_mem` `AddSubmonoid.add_mem` `AddSubmonoid.mem_closure_neg` `Set.union_neg` `neg_neg` `Set.union_comm` `AddSubmonoid.closure_le` `Set.union_subset_iff` `subset_closure` `neg_subset_closure`
`coe_add_of_left_le_normalizer_right` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	`SetLike.coe` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`sup_eq_closure_add` `Set.Subset.antisymm` `closure_induction''` `neg_add_rev` `add_assoc` `neg_add_cancel_left` `Set.add_mem_add` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `mem_normalizer_iff` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `add_zero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `mem_normalizer_iff''` `add_neg_cancel_left` `subset_closure`
`coe_add_of_right_le_normalizer_left` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	`SetLike.coe` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`set_add_normalizer_comm` `sup_comm` `coe_add_of_left_le_normalizer_right`
`iSup_induction` 📖	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—	`closure_induction''` `Set.mem_iUnion` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `iSup_eq_closure`
`iSup_induction'` 📖	—	`mem_iSup_of_mem` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `ZeroMemClass.zero_mem` `AddSubgroup` `instSetLike` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SetLike.instMembership`	—	—	`mem_iSup_of_mem` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `iSup_induction` `Exists.snd`
`inf_add_assoc` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `instSetLike` `instMin` `Set.instInter`	—	`Set.ext` `Set.mem_add` `Set.mem_inter_iff` `add_mem` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `SetLike.mem_coe` `add_neg_cancel_right`
`neg_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SetLike.coe` `AddSubgroup` `instSetLike` `closure`	—	`SetLike.mem_coe` `neg_mem_iff` `subset_closure` `Set.mem_neg`
`normal_add` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`coe_add_of_right_le_normalizer_left` `le_normalizer_of_normal`
`set_add_normal_comm` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup` `instSetLike`	—	`set_add_normalizer_comm` `subset_normalizer_of_normal`
`set_add_normalizer_comm` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `AddSubgroup` `instSetLike` `normalizer`	`Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Set.iUnion_add_left_image` `Set.iUnion_add_right_image` `Set.iUnion_congr_Prop` `Set.image_add_left` `Set.image_add_right` `mem_normalizer_iff'` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass`
`sup_eq_closure_add` 📖	mathematical	—	`AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `closure` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `instSetLike`	—	`le_antisymm` `sup_le` `subset_closure` `zero_mem` `add_zero` `zero_add` `LE.le.trans` `closure_add_le` `closure_eq` `le_refl`
`sup_normal` 📖	mathematical	—	`Normal` `AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`SetLike.mem_coe` `normal_add` `Normal.conj_mem` `add_assoc` `neg_add_cancel_left`
`toAddSubmonoid_zmultiples` 📖	mathematical	—	`toAddSubmonoid` `zmultiples` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice` `AddSubmonoid.multiples` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`zmultiples_eq_closure` `closure_toAddSubmonoid` `AddSubmonoid.closure_union` `AddSubmonoid.multiples_eq_closure` `Set.neg_singleton`
`vadd_mem_of_mem_closure_of_mem` 📖	—	`Set` `Set.instMembership` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddSubgroup` `SetLike.instMembership` `instSetLike` `closure`	—	—	`closure_induction''` `zero_vadd` `AddSemigroupAction.add_vadd`
`vadd_opposite_image_add_preimage` 📖	mathematical	—	`Set.image` `HVAdd.hVAdd` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `instSetLike` `op` `instHVAdd` `instVAdd` `Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`vadd_opposite_image_add_preimage'`
`vadd_opposite_image_add_preimage'` 📖	mathematical	—	`Set.image` `HVAdd.hVAdd` `AddOpposite` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Set.image_congr` `Set.image_add_right` `Set.preimage_preimage` `add_assoc`

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multiples_le_zmultiples` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `multiples` `AddSubgroup.toAddSubmonoid` `AddSubgroup.zmultiples`	—	`AddSubgroup.toAddSubmonoid_zmultiples` `le_sup_left`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroupClosure_add` 📖	mathematical	`Nonempty`	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.closure`	—	`iUnion_op_vadd_set` `op_vadd_coe_set` `AddSubgroup.instAddSubgroupClass` `AddSubgroup.subset_closure` `iUnion_congr_Prop` `biUnion_const`
`addSubgroupClosure_add_nsmul` 📖	mathematical	`Nonempty`	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.closure` `AddMonoid.toNatSMul` `addMonoid`	—	`zero_nsmul` `add_zero` `succ_nsmul'` `add_assoc` `addSubgroupClosure_add`
`add_addSubgroupClosure` 📖	mathematical	`Nonempty`	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.closure`	—	`vadd_eq_add` `iUnion_vadd_set` `vadd_coe_set` `AddSubgroup.instAddSubgroupClass` `AddSubgroup.subset_closure` `iUnion_congr_Prop` `biUnion_const`
`mul_subgroupClosure` 📖	mathematical	`Nonempty`	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.closure`	—	`smul_eq_mul` `iUnion_smul_set` `smul_coe_set` `Subgroup.instSubgroupClass` `Subgroup.subset_closure` `iUnion_congr_Prop` `biUnion_const`
`nsmul_add_addSubgroupClosure` 📖	mathematical	`Nonempty`	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toNatSMul` `addMonoid` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.closure`	—	`zero_nsmul` `zero_add` `succ_nsmul` `add_assoc` `add_addSubgroupClosure`
`pow_mul_subgroupClosure` 📖	mathematical	`Nonempty`	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toNatPow` `monoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.closure`	—	`pow_zero` `one_mul` `pow_succ` `mul_assoc` `mul_subgroupClosure`
`subgroupClosure_mul` 📖	mathematical	`Nonempty`	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.closure`	—	`iUnion_op_smul_set` `op_smul_coe_set` `Subgroup.instSubgroupClass` `Subgroup.subset_closure` `iUnion_congr_Prop` `biUnion_const`
`subgroupClosure_mul_pow` 📖	mathematical	`Nonempty`	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.closure` `Monoid.toNatPow` `monoid`	—	`pow_zero` `mul_one` `pow_succ'` `mul_assoc` `subgroupClosure_mul`

Subgroup

Definitions

Name	Category	Theorems
`equivSMul` 📖	CompOp	2 math math: `equivSMul_apply_coe`, `equivSMul_symm_apply_coe`
`pointwiseMulAction` 📖	CompOp	55 math math: `smul_mem_pointwise_smul_iff₀`, `pointwise_smul_le_pointwise_smul_iff`, `equivSMul_apply_coe`, `coe_pointwise_smul`, `Sylow.pointwise_smul_def`, `pointwise_smul_subset_iff`, `mem_pointwise_smul_iff_inv_smul_mem₀`, `subset_pointwise_smul_iff`, `CongruenceSubgroup.exists_Gamma_le_conj'`, `conj_smul_subgroupOf`, `CongruenceSubgroup.conjGL_coe`, `instCovariantClassHSMulLe`, `IsCusp.of_isFiniteRelIndex_conj`, `pointwise_smul_le_pointwise_smul_iff₀`, `Normal.conj_smul_eq_self`, `SlashInvariantForm.coe_translate`, `Normal.conjAct`, `Commensurable.commensurable_conj`, `pointwise_smul_def`, `conjAct_pointwise_smul_iff`, `Commensurable.commensurator_mem_iff`, `CongruenceSubgroup.IsArithmetic.conj`, `CongruenceSubgroup.Gamma_cong_eq_self`, `pointwise_isCentralScalar`, `mem_inv_pointwise_smul_iff₀`, `normalCore_eq_iInf_conjAct`, `CongruenceSubgroup.isArithmetic_conj_SL2Z`, `mem_smul_pointwise_iff_exists`, `CuspForm.coe_translate`, `conj_smul_le_of_le`, `Commensurable.commensurable_inv`, `Commensurable.conj`, `smul_closure`, `pointwise_smul_le_iff₀`, `smul_sup`, `smul_inf`, `conjAct_pointwise_smul_eq_self`, `Sylow.coe_subgroup_smul`, `IsGalois.map_fixingSubgroup`, `Commensurable.commensurator'_mem_iff`, `mem_inv_pointwise_smul_iff`, `CongruenceSubgroup.conj_cong_is_cong`, `conj_smul_eq_self_of_mem`, `smul_mem_pointwise_smul`, `relIndex_pointwise_smul`, `equivSMul_symm_apply_coe`, `ModularForm.coe_translate`, `MulAction.IwasawaStructure.is_conj`, `mem_pointwise_smul_iff_inv_smul_mem`, `smul_bot`, `le_pointwise_smul_iff₀`, `IsArithmetic.conj`, `pointwise_smul_toSubmonoid`, `IsCusp.smul`, `smul_mem_pointwise_smul_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_induction''` 📖	—	`subset_closure` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvMemClass.inv_mem` `Subgroup` `instSetLike` `SubgroupClass.toInvMemClass` `Group.toDivInvMonoid` `instSubgroupClass` `closure` `InvOneClass.toOne` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `SubgroupClass.toSubmonoidClass` `MulOne.toMul` `MulOneClass.toMulOne` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SetLike.instMembership`	—	—	`subset_closure` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `instSubgroupClass` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `closure_induction_left`
`closure_induction_left` 📖	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneMemClass.one_mem` `Subgroup` `instSetLike` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `closure` `MulOne.toMul` `MulOneClass.toMulOne` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `subset_closure` `InvOneClass.toInv` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `SetLike.instMembership`	—	—	`OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `subset_closure` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `closure_toSubmonoid` `Submonoid.closure_induction_left` `Submonoid.instSubmonoidClass` `Submonoid.subset_closure` `inv_inv`
`closure_induction_right` 📖	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneMemClass.one_mem` `Subgroup` `instSetLike` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `closure` `MulOne.toMul` `MulOneClass.toMulOne` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `subset_closure` `InvOneClass.toInv` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `SetLike.instMembership`	—	—	`OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `subset_closure` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `closure_induction_left` `op_closure`
`closure_inv` 📖	mathematical	—	`closure` `Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`closure_toSubmonoid` `inv_inv` `Set.union_comm`
`closure_mul_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`sInf_le` `mul_mem` `SetLike.le_def` `instIsConcreteLE` `le_sup_left` `subset_closure` `le_sup_right`
`closure_pow` 📖	mathematical	`Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`closure` `Set.NPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`LE.le.antisymm` `closure_pow_le` `closure_mono` `Set.subset_pow`
`closure_pow_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Monoid.toNatPow` `Set.monoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`pow_zero` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `pow_succ` `le_imp_le_of_le_of_le` `closure_mul_le` `le_refl` `sup_le_sup` `sup_idem`
`closure_singleton_inv` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.inv_singleton` `closure_inv`
`closure_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `closure` `Submonoid.closure` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set` `Set.instUnion` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`le_antisymm` `closure_induction` `Submonoid.closure_mono` `Set.subset_union_left` `Submonoid.subset_closure` `Submonoid.one_mem` `Submonoid.mul_mem` `Submonoid.mem_closure_inv` `Set.union_inv` `inv_inv` `Set.union_comm` `Submonoid.closure_le`
`coe_mul_of_left_le_normalizer_right` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	`SetLike.coe` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`sup_eq_closure_mul` `Set.Subset.antisymm` `closure_induction''` `mul_inv_rev` `mul_assoc` `inv_mul_cancel_left` `Set.mul_mem_mul` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `instSubgroupClass` `mem_normalizer_iff` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `mul_one` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `mem_normalizer_iff''` `mul_inv_cancel_left` `subset_closure`
`coe_mul_of_right_le_normalizer_left` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalizer`	`SetLike.coe` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`set_mul_normalizer_comm` `sup_comm` `coe_mul_of_left_le_normalizer_right`
`coe_pointwise_smul` 📖	mathematical	—	`SetLike.coe` `Subgroup` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Set` `Set.smulSet` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`conjAct_pointwise_smul_eq_self` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike` `normalizer`	`ConjAct` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `ConjAct.instMulDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct`	—	`conjAct_pointwise_smul_iff`
`conjAct_pointwise_smul_iff` 📖	mathematical	—	`ConjAct` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `ConjAct.instMulDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct` `SetLike.instMembership` `instSetLike` `normalizer`	—	`inv_mem_iff` `inv_inv`
`conj_smul_eq_self_of_mem` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj`	—	`le_antisymm` `conj_smul_le_of_le` `le_refl` `subset_pointwise_smul_iff` `map_inv` `MonoidHom.instMonoidHomClass` `inv_mem`
`conj_smul_le_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj` `SetLike.instMembership` `instSetLike`	—	`mul_mem` `inv_mem`
`conj_smul_subgroupOf` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`MulAut` `SetLike.instMembership` `instSetLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj` `subgroupOf`	—	`le_antisymm`
`equivSMul_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `EquivLike.toEquiv` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulEquiv.instEquivLike` `MulDistribMulAction.toMulEquiv` `SetLike.coe` `Submonoid` `Submonoid.instSetLike` `toSubmonoid` `Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `mul` `equivSMul` `MulDistribMulAction.toMulAction`	—	—
`equivSMul_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.instSetLike` `toSubmonoid` `DFunLike.coe` `MulEquiv` `Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivSMul` `MulDistribMulAction.toMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.image` `MulOne.toMul` `MulOneClass.toMulOne` `MulDistribMulAction.toMulEquiv`	—	—
`iSup_induction` 📖	—	`Subgroup` `SetLike.instMembership` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—	`closure_induction''` `Set.mem_iUnion` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `instSubgroupClass` `iSup_eq_closure`
`iSup_induction'` 📖	—	`mem_iSup_of_mem` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneMemClass.one_mem` `Subgroup` `instSetLike` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `MulOne.toMul` `MulOneClass.toMulOne` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SetLike.instMembership`	—	—	`mem_iSup_of_mem` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `iSup_induction` `Exists.snd`
`inf_mul_assoc` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike` `instMin` `Set.instInter`	—	`Set.ext` `mul_mem` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `mul_inv_cancel_right`
`instCovariantClassHSMulLe` 📖	mathematical	—	`CovariantClass` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`Set.image_mono`
`inv_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SetLike.coe` `Subgroup` `instSetLike` `closure`	—	`SetLike.mem_coe` `inv_mem_iff` `subset_closure` `Set.mem_inv`
`mem_inv_pointwise_smul_iff` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulDistribMulAction.toMulAction`	—	`Set.mem_inv_smul_set_iff`
`mem_pointwise_smul_iff_inv_smul_mem` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.mem_smul_set_iff_inv_smul_mem`
`mem_smul_pointwise_iff_exists` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.mem_smul_set`
`mul_inf_assoc` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike` `instMin` `Set.instInter`	—	`Set.ext` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `inv_mul_cancel_left`
`mul_normal` 📖	mathematical	—	`SetLike.coe` `Subgroup` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`coe_mul_of_left_le_normalizer_right` `le_normalizer_of_normal`
`normalCore_eq_iInf_conjAct` 📖	mathematical	—	`normalCore` `iInf` `Subgroup` `ConjAct` `instInfSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `ConjAct.instMulDistribMulAction`	—	`ext` `inv_inv`
`normal_mul` 📖	mathematical	—	`SetLike.coe` `Subgroup` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`coe_mul_of_right_le_normalizer_left` `le_normalizer_of_normal`
`pointwise_isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulOpposite` `MulOpposite.instMonoid`	—	`MonoidHom.ext` `IsCentralScalar.op_smul_eq_smul`
`pointwise_smul_def` 📖	mathematical	—	`Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `map` `DFunLike.coe` `MonoidHom` `Monoid.End` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.End.instMonoid` `MonoidHom.instFunLike` `MulDistribMulAction.toMonoidEnd`	—	—
`pointwise_smul_le_pointwise_smul_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction`	—	`Set.smul_set_subset_smul_set_iff`
`pointwise_smul_subset_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.smul_set_subset_iff_subset_inv_smul_set`
`pointwise_smul_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.pointwiseMulAction`	—	—
`set_mul_normal_comm` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `instSetLike`	—	`set_mul_normalizer_comm` `subset_normalizer_of_normal`
`set_mul_normalizer_comm` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Subgroup` `instSetLike` `normalizer`	`Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.iUnion_mul_left_image` `Set.iUnion_mul_right_image` `Set.iUnion_congr_Prop` `Set.image_mul_left` `Set.image_mul_right` `mem_normalizer_iff'` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `instSubgroupClass`
`singleton_mul_subgroup` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.instSingletonSet` `SetLike.coe`	—	`Set.singleton_mul` `Set.image_mul_left` `mul_mem_cancel_left` `instSubgroupClass` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass`
`smul_bot` 📖	mathematical	—	`Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Bot.bot` `instBot`	—	`map_bot`
`smul_closure` 📖	mathematical	—	`Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `closure` `Set` `Set.smulSet` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`MonoidHom.map_closure`
`smul_inf` 📖	mathematical	—	`Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `instMin`	—	—
`smul_mem_of_mem_closure_of_mem` 📖	—	`Set` `Set.instMembership` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup` `SetLike.instMembership` `instSetLike` `closure`	—	—	`closure_induction''` `one_smul` `SemigroupAction.mul_smul`
`smul_mem_pointwise_smul` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Set.smul_mem_smul_set`
`smul_mem_pointwise_smul_iff` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction`	—	`Set.smul_mem_smul_set_iff`
`smul_opposite_image_mul_preimage` 📖	mathematical	—	`Set.image` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `instSetLike` `op` `instSMul` `Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`smul_opposite_image_mul_preimage'`
`smul_opposite_image_mul_preimage'` 📖	mathematical	—	`Set.image` `MulOpposite` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Set.image_congr` `Set.image_mul_right` `Set.preimage_preimage` `mul_assoc`
`smul_sup` 📖	mathematical	—	`Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`map_sup`
`subgroup_mul_singleton` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Set.instSingletonSet`	—	`Set.mul_singleton` `Set.image_mul_right` `mul_mem_cancel_right` `instSubgroupClass` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass`
`subset_pointwise_smul_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.subset_smul_set_iff`
`sup_eq_closure_mul` 📖	mathematical	—	`Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `closure` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `instSetLike`	—	`le_antisymm` `sup_le` `subset_closure` `one_mem` `mul_one` `one_mul` `LE.le.trans` `closure_mul_le` `closure_eq` `le_refl`
`sup_normal` 📖	mathematical	—	`Normal` `Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`SetLike.mem_coe` `normal_mul` `Normal.conj_mem` `mul_assoc` `inv_mul_cancel_left`
`toSubmonoid_zpowers` 📖	mathematical	—	`toSubmonoid` `zpowers` `Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice` `Submonoid.powers` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`zpowers_eq_closure` `closure_toSubmonoid` `Submonoid.closure_union` `Submonoid.powers_eq_closure` `Set.inv_singleton`

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjAct` 📖	mathematical	—	`ConjAct` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup.pointwiseMulAction` `ConjAct.instMulDistribMulAction`	—	`Subgroup.map_le_iff_le_comap` `conj_mem` `LE.le.antisymm` `Eq.trans_le` `smul_inv_smul` `Subgroup.map_mono`
`conj_smul_eq_self` 📖	mathematical	—	`MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `Subgroup.pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj`	—	`conjAct`
`of_conjugate_fixed` 📖	mathematical	`MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `Subgroup.pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj`	`Subgroup.Normal`	—	`Subgroup.mem_pointwise_smul_iff_inv_smul_mem` `map_inv` `MonoidHom.instMonoidHomClass` `MulAut.smul_def` `MulAut.conj_apply` `inv_inv` `mul_assoc` `inv_mul_cancel` `mul_one` `one_mul`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powers_le_zpowers` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `powers` `Subgroup.toSubmonoid` `Subgroup.zpowers`	—	`Subgroup.toSubmonoid_zpowers` `le_sup_left`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div_coe` 📖	mathematical	—	`Set` `Set.div` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `SetLike.coe`	—	`div_eq_mul_inv` `inv_coe_set` `SubgroupClass.toInvMemClass` `coe_mul_coe` `SubgroupClass.toSubmonoidClass`
`coe_set_eq_one` 📖	mathematical	—	`SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Bot.bot` `Subgroup.instBot`	—	`SetLike.ext'_iff`
`coe_set_eq_zero` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Bot.bot` `AddSubgroup.instBot`	—	`SetLike.ext'_iff`
`coe_sub_coe` 📖	mathematical	—	`Set` `Set.sub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `SetLike.coe`	—	`sub_eq_add_neg` `neg_coe_set` `AddSubgroupClass.toNegMemClass` `coe_add_coe` `AddSubgroupClass.toAddSubmonoidClass`
`inv_coe_set` 📖	mathematical	—	`Set` `Set.inv` `InvolutiveInv.toInv` `SetLike.coe`	—	`Set.ext` `inv_mem_iff`
`neg_coe_set` 📖	mathematical	—	`Set` `Set.neg` `InvolutiveNeg.toNeg` `SetLike.coe`	—	`Set.ext` `neg_mem_iff`
`op_smul_coe_set` 📖	mathematical	`SetLike.instMembership`	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe`	—	`Set.ext` `SubgroupClass.toInvMemClass`
`op_vadd_coe_set` 📖	mathematical	`SetLike.instMembership`	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe`	—	`Set.ext` `Set.mem_vadd_set_iff_neg_vadd_mem` `SetLike.mem_coe` `add_mem_cancel_right` `neg_mem_iff` `AddSubgroupClass.toNegMemClass`
`smul_coe_set` 📖	mathematical	`SetLike.instMembership`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe`	—	`Set.ext` `SubgroupClass.toInvMemClass`
`vadd_coe_set` 📖	mathematical	`SetLike.instMembership`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe`	—	`Set.ext` `Set.mem_vadd_set_iff_neg_vadd_mem` `SetLike.mem_coe` `add_mem_cancel_left` `neg_mem_iff` `AddSubgroupClass.toNegMemClass`

---

← Back to Index