SubMulAction

📁 Source: Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Statistics

Metric	Count
Definitions `SMulMemClass`, `smul`, `smul'`, `vadd`, `vadd'`, `SubAddAction`, `subtype`, `toAddAction`, `addAction`, `addAction'`, `carrier`, `copy`, `inclusion`, `instBot`, `instCompl`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instMax`, `instMin`, `instPartialOrder`, `instSetLike`, `instSupSet`, `instTop`, `instVAddSubtypeMem`, `subtype`, `vadd'`, `SubMulAction`, `subtype`, `toMulAction`, `carrier`, `copy`, `inclusion`, `instBot`, `instCompl`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instMax`, `instMin`, `instNegSubtypeMem`, `instPartialOrder`, `instSMulSubtypeMem`, `instSetLike`, `instSupSet`, `instTop`, `instZeroSubtypeMemOfNonempty`, `mulAction`, `mulAction'`, `smul'`, `subtype`, `instMulActionSubtypeNeOfNat`, `nonZeroSubMul`, `VAddMemClass`, `fixedPointsSubAddOfNormal`, `fixedPointsSubMulOfNormal`, `instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal`	57
Theorems `zsmulMemClass`, `nsmulMemClass`, `ofIsScalarTower`, `smul_mem`, `forall_smul_mem_iff`, `instIsCancelSMulSubtypeMem`, `instIsCancelVAddSubtypeMem`, `instIsLeftCancelSMulSubtypeMem`, `instIsLeftCancelVAddSubtypeMem`, `instIsScalarTower`, `instIsScalarTowerSubtypeMem`, `instSMulCommClass`, `instSMulCommClassSubtypeMem`, `instSMulCommClassSubtypeMem_1`, `instSMulCommClassSubtypeMem_2`, `instVAddCommClassSubtypeMem`, `instVAddCommClassSubtypeMem_1`, `instVAddCommClassSubtypeMem_2`, `mk_smul_mk`, `mk_smul_of_tower_mk`, `mk_vadd_mk`, `mk_vadd_of_tower_mk`, `smul_def`, `smul_of_tower_def`, `vadd_def`, `vadd_of_tower_def`, `val_smul`, `val_smul_of_tower`, `val_vadd`, `val_vadd_of_tower`, `coe_subtype`, `coe_copy`, `compl_def`, `copy_eq`, `ext`, `ext_iff`, `image_inclusion`, `coe_eq`, `toFun_eq_coe`, `inclusion_injective`, `instVAddMemClass`, `isCentralVAdd`, `mem_carrier`, `mem_iInf`, `mem_iSup`, `mem_orbit_subAdd_iff`, `orbitRel_of_subAdd`, `stabilizer_of_subAdd`, `addSubmonoid`, `subtype_apply`, `subtype_eq_val`, `vaddAssocClass`, `vaddAssocClass'`, `vadd_mem`, `vadd_mem'`, `vadd_mem_iff'`, `vadd_of_tower_mem`, `val_image_orbit`, `val_preimage_orbit`, `val_vadd`, `val_vadd_of_tower`, `coe_subtype`, `subtype_apply`, `subtype_injective`, `coe_copy`, `compl_def`, `copy_eq`, `ext`, `ext_iff`, `image_inclusion`, `coe_eq`, `toFun_eq_coe`, `inclusion_injective`, `instSMulMemClass`, `isCentralScalar`, `isScalarTower`, `isScalarTower'`, `mem_carrier`, `mem_iInf`, `mem_iSup`, `mem_orbit_subMul_iff`, `neg_mem`, `neg_mem_iff`, `orbitRel_of_subMul`, `smul_mem`, `smul_mem'`, `smul_mem_iff`, `smul_mem_iff'`, `smul_of_tower_mem`, `stabilizer_of_subMul`, `submonoid`, `subtype_apply`, `subtype_eq_val`, `subtype_injective`, `val_image_orbit`, `val_neg`, `val_preimage_orbit`, `val_smul`, `val_smul_of_tower`, `zero_mem`, `orbitRel_nonZero_iff`, `smul_coe`, `ofVAddAssocClass`, `vadd_mem`, `coe_smul_fixedPoints_of_normal`, `smul_mem_fixedPoints_of_normal`, `vadd_mem_fixedPoints_of_normal`	107
Total	164

AddSubgroupClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zsmulMemClass` 📖	mathematical	—	`SMulMemClass` `SubNegMonoid.toZSMul`	—	`zsmul_mem`

AddSubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmulMemClass` 📖	mathematical	—	`SMulMemClass` `AddMonoid.toNatSMul`	—	`nsmul_mem`

SMulMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofIsScalarTower` 📖	mathematical	—	`SMulMemClass`	—	`smul_mem` `smul_one_smul`
`smul_mem` 📖	—	`SetLike.instMembership`	—	—	—

SetLike

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	10 math math: `instSMulCommClass`, `instIsCancelSMulSubtypeMem`, `smul_def`, `instIsScalarTower`, `instIsLeftCancelSMulSubtypeMem`, `val_smul`, `SMulMemClass.continuousSMul`, `mk_smul_mk`, `instSMulCommClassSubtypeMem`, `StarMemClass.instStarModule`
`smul'` 📖	CompOp	14 math math: `Subalgebra.inclusion.isScalarTower_left`, `Subalgebra.isScalarTower_right`, `Subalgebra.coe_smul`, `Subalgebra.isScalarTower_mid`, `val_smul_of_tower`, `NonUnitalStarSubalgebra.coe_smul`, `IntermediateField.coe_smul`, `mk_smul_of_tower_mk`, `smul_of_tower_def`, `IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin`, `NonUnitalSubalgebra.coe_smul`, `instSMulCommClassSubtypeMem_1`, `instIsScalarTowerSubtypeMem`, `instSMulCommClassSubtypeMem_2`
`vadd` 📖	CompOp	7 math math: `val_vadd`, `VAddMemClass.continuousVAdd`, `instVAddCommClassSubtypeMem`, `vadd_def`, `mk_vadd_mk`, `instIsLeftCancelVAddSubtypeMem`, `instIsCancelVAddSubtypeMem`
`vadd'` 📖	CompOp	5 math math: `vadd_of_tower_def`, `val_vadd_of_tower`, `instVAddCommClassSubtypeMem_1`, `instVAddCommClassSubtypeMem_2`, `mk_vadd_of_tower_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_smul_mem_iff` 📖	mathematical	—	`instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`one_smul` `SMulMemClass.smul_mem`
`instIsCancelSMulSubtypeMem` 📖	mathematical	—	`IsCancelSMul` `instMembership` `smul`	—	`instIsLeftCancelSMulSubtypeMem` `IsCancelSMul.toIsLeftCancelSMul` `IsCancelSMul.right_cancel`
`instIsCancelVAddSubtypeMem` 📖	mathematical	—	`IsCancelVAdd` `instMembership` `vadd`	—	`instIsLeftCancelVAddSubtypeMem` `IsCancelVAdd.toIsLeftCancelVAdd` `IsCancelVAdd.right_cancel`
`instIsLeftCancelSMulSubtypeMem` 📖	mathematical	—	`IsLeftCancelSMul` `instMembership` `smul`	—	`IsLeftCancelSMul.left_cancel`
`instIsLeftCancelVAddSubtypeMem` 📖	mathematical	—	`IsLeftCancelVAdd` `instMembership` `vadd`	—	`IsLeftCancelVAdd.left_cancel`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `instMembership` `smul` `MulMemClass.mul`	—	`smul_assoc`
`instIsScalarTowerSubtypeMem` 📖	mathematical	—	`IsScalarTower` `instMembership` `smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `instMembership` `smul` `MulMemClass.mul`	—	`SMulCommClass.smul_comm`
`instSMulCommClassSubtypeMem` 📖	mathematical	—	`SMulCommClass` `instMembership` `smul`	—	`SMulCommClass.smul_comm`
`instSMulCommClassSubtypeMem_1` 📖	mathematical	—	`SMulCommClass` `instMembership` `smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `SMulCommClass.smul_comm`
`instSMulCommClassSubtypeMem_2` 📖	mathematical	—	`SMulCommClass` `instMembership` `smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `SMulCommClass.smul_comm`
`instVAddCommClassSubtypeMem` 📖	mathematical	—	`VAddCommClass` `instMembership` `vadd`	—	`VAddCommClass.vadd_comm`
`instVAddCommClassSubtypeMem_1` 📖	mathematical	—	`VAddCommClass` `instMembership` `vadd'` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `VAddCommClass.vadd_comm`
`instVAddCommClassSubtypeMem_2` 📖	mathematical	—	`VAddCommClass` `instMembership` `vadd'` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `VAddCommClass.vadd_comm`
`mk_smul_mk` 📖	mathematical	`instMembership`	`smul` `SMulMemClass.smul_mem`	—	—
`mk_smul_of_tower_mk` 📖	mathematical	`instMembership`	`smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulMemClass.smul_mem` `smul_one_smul`	—	—
`mk_vadd_mk` 📖	mathematical	`instMembership`	`HVAdd.hVAdd` `instHVAdd` `vadd` `VAddMemClass.vadd_mem`	—	—
`mk_vadd_of_tower_mk` 📖	mathematical	`instMembership`	`HVAdd.hVAdd` `instHVAdd` `vadd'` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `VAddMemClass.vadd_mem` `vadd_zero_vadd`	—	—
`smul_def` 📖	mathematical	—	`instMembership` `smul` `SMulMemClass.smul_mem`	—	—
`smul_of_tower_def` 📖	mathematical	—	`instMembership` `smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulMemClass.smul_mem` `smul_one_smul`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instMembership` `instHVAdd` `vadd` `VAddMemClass.vadd_mem`	—	—
`vadd_of_tower_def` 📖	mathematical	—	`HVAdd.hVAdd` `instMembership` `instHVAdd` `vadd'` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `VAddMemClass.vadd_mem` `vadd_zero_vadd`	—	—
`val_smul` 📖	mathematical	—	`instMembership` `smul`	—	—
`val_smul_of_tower` 📖	mathematical	—	`instMembership` `smul'`	—	—
`val_vadd` 📖	mathematical	—	`instMembership` `HVAdd.hVAdd` `instHVAdd` `vadd`	—	—
`val_vadd_of_tower` 📖	mathematical	—	`instMembership` `HVAdd.hVAdd` `instHVAdd` `vadd'`	—	—

SubAddAction

Definitions

Name	Category	Theorems
`addAction` 📖	CompOp	18 math math: `map_ofFixingAddSubgroupUnion_bijective`, `ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `ofFixingAddSubgroup.isMultiplyPretransitive`, `ofFixingAddSubgroup.isMultiplyPretransitive'`, `stabilizer_of_subMul.addSubmonoid`, `ofFixingAddSubgroup_insert_map_bijective`, `ofStabilizer.isMultiplyPretransitive_iff`, `ofFixingAddSubgroup_insert_map_apply`, `AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `fixingAddSubgroup_of_insert`, `orbitRel_of_subAdd`, `AddAction.ofFixingSubgroup.isMultiplyPreprimitive`, `ofStabilizer.isMultiplyPretransitive`, `stabilizer_of_subAdd`, `AddAction.isPreprimitive_fixingAddSubgroup_insert_iff`, `AddAction.isMultiplyPreprimitive_ofStabilizer`, `mem_ofFixingAddSubgroup_insert_iff`, `map_ofFixingAddSubgroupUnion_def`
`addAction'` 📖	CompOp	—
`carrier` 📖	CompOp	5 math math: `image_inclusion`, `compl_def`, `ofFixingAddSubgroup_carrier`, `mem_carrier`, `ofStabilizer_carrier`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`inclusion` 📖	CompOp	4 math math: `image_inclusion`, `inclusion.coe_eq`, `inclusion_injective`, `inclusion.toFun_eq_coe`
`instBot` 📖	CompOp	—
`instCompl` 📖	CompOp	1 math math: `compl_def`
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `mem_iInf`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	5 math math: `closure_mono`, `AddSemigroupIdeal.closure_le`, `AddSemigroupIdeal.instWellFoundedGT`, `AddSemigroupIdeal.closure_mono`, `closure_le`
`instSetLike` 📖	CompOp	82 math math: `map_ofFixingAddSubgroupUnion_bijective`, `AddSemigroupIdeal.mem_closure`, `notMem_val_image`, `subtype_apply`, `AddSemigroupIdeal.subset_closure`, `ofStabilizer.conjMap_comp`, `ofFixingAddSubgroup_of_inclusion_injective`, `subtype_eq_val`, `ofFixingAddSubgroup_of_singleton_bijective`, `mem_ofStabilizer_iff`, `ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `AddSemigroupIdeal.closure_le`, `AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff`, `ofStabilizer.conjMap_comp_neg_apply`, `instVAddMemClass`, `ofFixingAddSubgroup.isMultiplyPretransitive`, `ofFixingAddSubgroup.isMultiplyPretransitive'`, `ofStabilizer.isPretransitive_iff`, `stabilizer_of_subMul.addSubmonoid`, `conjMap_ofFixingAddSubgroup_bijective`, `AddSemigroupIdeal.coe_closure`, `conjMap_ofFixingAddSubgroup_coe_apply`, `ofFixingAddSubgroup_of_eq_bijective`, `vaddAssocClass'`, `subset_closure`, `val_image_orbit`, `AddSemigroupIdeal.coe_closure'`, `ofFixingAddSubgroup_insert_map_bijective`, `nat_card_ofStabilizer_eq`, `ofFixingAddSubgroup_of_eq_apply`, `AddSemigroupIdeal.mem_closure''`, `isCentralVAdd`, `AddSemigroupIdeal.mem_closure_of_mem`, `vadd_mem_iff'`, `ofStabilizer.isMultiplyPretransitive_iff`, `ofStabilizer.conjMap_bijective`, `val_preimage_orbit`, `image_inclusion`, `mem_iInf`, `mem_orbit_subAdd_iff`, `compl_def`, `AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `ofStabilizer.snoc_castSucc`, `mem_iSup`, `ENat_card_ofStabilizer_add_zero_eq`, `mem_closure`, `fixingAddSubgroup_of_insert`, `AddSemigroupIdeal.mem_closure'`, `orbitRel_of_subAdd`, `mem_ofFixingAddSubgroup_iff`, `ofFixingAddSubgroupEmpty_equivariantMap_bijective`, `inclusion.coe_eq`, `ext_iff`, `ofStabilizer.neg_conjMap_comp_apply`, `vaddAssocClass`, `AddAction.isMultiplyPreprimitive_iff`, `mem_carrier`, `ofFixingAddSubgroup.append_right`, `ofFixingAddSubgroup_equivariantMap_injective`, `mem_closure_of_mem`, `val_vadd`, `AddAction.ofFixingSubgroup.isMultiplyPreprimitive`, `nat_card_ofStabilizer_add_zero_eq`, `AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup`, `disjoint_val_image`, `AddAction.IsBlock.subtype_val_preimage`, `ofStabilizer.conjMap_comp_apply`, `val_vadd_of_tower`, `ofStabilizer.isMultiplyPretransitive`, `inclusion_injective`, `stabilizer_of_subAdd`, `AddAction.isPreprimitive_fixingAddSubgroup_insert_iff`, `closure_le`, `AddAction.isMultiplyPreprimitive_ofStabilizer`, `AddAction.isBlock_subtypeVal`, `mem_ofFixingAddSubgroup_insert_iff`, `AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff`, `inclusion.toFun_eq_coe`, `not_mem_of_mem_ofFixingAddSubgroup`, `ofStabilizer.isPretransitive_iff_of_conj`, `map_ofFixingAddSubgroupUnion_def`, `ofStabilizer.conjMap_apply`
`instSupSet` 📖	CompOp	1 math math: `mem_iSup`
`instTop` 📖	CompOp	—
`instVAddSubtypeMem` 📖	CompOp	3 math math: `subtype_apply`, `subtype_eq_val`, `val_vadd`
`subtype` 📖	CompOp	2 math math: `subtype_apply`, `subtype_eq_val`
`vadd'` 📖	CompOp	38 math math: `map_ofFixingAddSubgroupUnion_bijective`, `ofStabilizer.conjMap_comp`, `ofFixingAddSubgroup_of_inclusion_injective`, `ofFixingAddSubgroup_of_singleton_bijective`, `AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff`, `ofStabilizer.conjMap_comp_neg_apply`, `ofStabilizer.isPretransitive_iff`, `conjMap_ofFixingAddSubgroup_bijective`, `conjMap_ofFixingAddSubgroup_coe_apply`, `ofFixingAddSubgroup_of_eq_bijective`, `vaddAssocClass'`, `val_image_orbit`, `ofFixingAddSubgroup_insert_map_bijective`, `ofFixingAddSubgroup_of_eq_apply`, `isCentralVAdd`, `ofStabilizer.conjMap_bijective`, `ofFixingAddSubgroup_insert_map_apply`, `val_preimage_orbit`, `image_inclusion`, `mem_orbit_subAdd_iff`, `ofFixingAddSubgroupEmpty_equivariantMap_bijective`, `inclusion.coe_eq`, `ofStabilizer.neg_conjMap_comp_apply`, `vaddAssocClass`, `AddAction.isMultiplyPreprimitive_iff`, `ofFixingAddSubgroup_equivariantMap_injective`, `AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup`, `AddAction.IsBlock.subtype_val_preimage`, `ofStabilizer.conjMap_comp_apply`, `val_vadd_of_tower`, `inclusion_injective`, `AddAction.isPreprimitive_fixingAddSubgroup_insert_iff`, `AddAction.isBlock_subtypeVal`, `AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff`, `inclusion.toFun_eq_coe`, `ofStabilizer.isPretransitive_iff_of_conj`, `map_ofFixingAddSubgroupUnion_def`, `ofStabilizer.conjMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`SetLike.coe` `SubAddAction` `instSetLike`	`copy`	—	—
`compl_def` 📖	mathematical	—	`carrier` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Compl.compl` `SubAddAction` `instCompl` `Set` `Set.instCompl` `SetLike.coe` `instSetLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `SubAddAction` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`SubAddAction` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`SubAddAction` `SetLike.instMembership` `instSetLike`	—	`ext`
`image_inclusion` 📖	mathematical	—	`Set.range` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddActionHom` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left` `instFunLikeAddActionHom` `inclusion` `carrier`	—	`VAddAssocClass.left` `inclusion.coe_eq` `Subtype.range_coe`
`inclusion_injective` 📖	mathematical	—	`SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddActionHom` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left` `instFunLikeAddActionHom` `inclusion`	—	`Subtype.val_injective`
`instVAddMemClass` 📖	mathematical	—	`VAddMemClass` `SubAddAction` `instSetLike`	—	`vadd_mem'`
`isCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `vadd'` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `SetLike.coe` `SubAddAction` `instSetLike`	—	—
`mem_iInf` 📖	mathematical	—	`SubAddAction` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	`Set.iInter_congr_Prop` `Set.mem_range` `Set.iInter_exists` `Set.iInter_iInter_eq'` `Set.mem_iInter` `SetLike.mem_coe`
`mem_iSup` 📖	mathematical	—	`SubAddAction` `SetLike.instMembership` `instSetLike` `iSup` `instSupSet`	—	`Set.iUnion_congr_Prop` `Set.mem_range` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `Set.mem_iUnion` `SetLike.mem_coe`
`mem_orbit_subAdd_iff` 📖	mathematical	—	`SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership` `AddAction.orbit` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `val_preimage_orbit` `Set.mem_preimage`
`orbitRel_of_subAdd` 📖	mathematical	—	`AddAction.orbitRel` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `addAction` `Setoid.comap`	—	`Setoid.ext_iff` `Setoid.comap_rel` `mem_orbit_subAdd_iff`
`stabilizer_of_subAdd` 📖	mathematical	—	`AddAction.stabilizer` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `addAction`	—	`stabilizer_of_subMul.addSubmonoid`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `AddActionHom` `SubAddAction` `SetLike.instMembership` `instSetLike` `instVAddSubtypeMem` `instFunLikeAddActionHom` `subtype`	—	—
`subtype_eq_val` 📖	mathematical	—	`DFunLike.coe` `AddActionHom` `SubAddAction` `SetLike.instMembership` `instSetLike` `instVAddSubtypeMem` `instFunLikeAddActionHom` `subtype`	—	—
`vaddAssocClass` 📖	mathematical	—	`VAddAssocClass` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `vadd_assoc`
`vaddAssocClass'` 📖	mathematical	—	`VAddAssocClass` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `vadd'`	—	`vadd_assoc`
`vadd_mem` 📖	mathematical	`SubAddAction` `SetLike.instMembership` `instSetLike`	`HVAdd.hVAdd` `instHVAdd`	—	`vadd_mem'`
`vadd_mem'` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`HVAdd.hVAdd` `instHVAdd`	—	—
`vadd_mem_iff'` 📖	mathematical	—	`SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `HVAdd.hVAdd` `instHVAdd` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`vadd_of_tower_mem` `neg_vadd_vadd`
`vadd_of_tower_mem` 📖	mathematical	`SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike`	`HVAdd.hVAdd` `instHVAdd`	—	`zero_vadd` `vadd_assoc` `vadd_mem`
`val_image_orbit` 📖	mathematical	—	`Set.image` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `AddAction.orbit` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `Set.range_comp`
`val_preimage_orbit` 📖	mathematical	—	`Set.preimage` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `AddAction.orbit` `vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `val_image_orbit` `Function.Injective.preimage_image` `Subtype.val_injective`
`val_vadd` 📖	mathematical	—	`SubAddAction` `SetLike.instMembership` `instSetLike` `HVAdd.hVAdd` `instHVAdd` `instVAddSubtypeMem`	—	—
`val_vadd_of_tower` 📖	mathematical	—	`SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `instSetLike` `HVAdd.hVAdd` `instHVAdd` `vadd'`	—	—

SubAddAction.SMulMemClass

Definitions

Name	Category	Theorems
`subtype` 📖	CompOp	1 math math: `coe_subtype`
`toAddAction` 📖	CompOp	1 math math: `coe_subtype`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `AddActionHom` `SetLike.instMembership` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `toAddAction` `instFunLikeAddActionHom` `subtype`	—	—

SubAddAction.inclusion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq` 📖	mathematical	—	`DFunLike.coe` `AddActionHom` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `SubAddAction.instSetLike` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left` `instFunLikeAddActionHom` `SubAddAction.inclusion`	—	`VAddAssocClass.left`
`toFun_eq_coe` 📖	mathematical	—	`AddActionHom.toFun` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `SubAddAction.instSetLike` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left` `SubAddAction.inclusion`	—	`VAddAssocClass.left`

SubAddAction.stabilizer_of_subMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubmonoid` 📖	mathematical	—	`AddAction.stabilizerAddSubmonoid` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `SetLike.instMembership` `SubAddAction.instSetLike` `SubAddAction.addAction`	—	`AddSubmonoid.ext` `AddAction.mem_stabilizerAddSubmonoid_iff` `SetLike.coe_eq_coe`

SubMulAction

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	5 math math: `ofStabilizer_carrier`, `mem_carrier`, `ofFixingSubgroup_carrier`, `compl_def`, `image_inclusion`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`inclusion` 📖	CompOp	4 math math: `inclusion.toFun_eq_coe`, `inclusion_injective`, `inclusion.coe_eq`, `image_inclusion`
`instBot` 📖	CompOp	—
`instCompl` 📖	CompOp	1 math math: `compl_def`
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `mem_iInf`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instNegSubtypeMem` 📖	CompOp	1 math math: `val_neg`
`instPartialOrder` 📖	CompOp	7 math math: `closure_le`, `SemigroupIdeal.instWellFoundedGT`, `SemigroupIdeal.closure_le`, `Submodule.toSubMulAction_strictMono`, `SemigroupIdeal.closure_mono`, `closure_mono`, `Submodule.toSubMulAction_mono`
`instSMulSubtypeMem` 📖	CompOp	4 math math: `subtype_eq_val`, `subtype_injective`, `subtype_apply`, `val_smul`
`instSetLike` 📖	CompOp	103 math math: `ofStabilizer.isPretransitive_iff_of_conj`, `MulAction.isPreprimitive_of_fixingSubgroup_empty_iff`, `ofStabilizer.conjMap_comp_apply`, `subtype_eq_val`, `ofFixingSubgroup_equivariantMap_injective`, `closure_le`, `ofStabilizer.conjMap_comp_inv_apply`, `mem_closure_of_mem`, `ofFixingSubgroup_of_inclusion_injective`, `subset_coe_pow`, `nat_card_ofStabilizer_add_one_eq`, `SemigroupIdeal.mem_closure''`, `ofStabilizer.inv_conjMap_comp_apply`, `SemigroupIdeal.subset_closure`, `mem_iSup`, `map_ofFixingSubgroupUnion_def`, `ofStabilizer.isMultiplyPretransitive_iff`, `subtype_injective`, `MulAction.ofFixingSubgroup.isMultiplyPreprimitive`, `ofStabilizer.isPretransitive_iff`, `mem_carrier`, `stabilizer_of_subMul`, `mem_mul`, `fixingSubgroup_of_insert`, `SemigroupIdeal.coe_closure`, `MulAction.isPreprimitive_ofFixingSubgroup_conj_iff`, `ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `stabilizer_of_subMul.submonoid`, `inclusion.toFun_eq_coe`, `disjoint_val_image`, `algebraMap_mem`, `StrongDual.polarSubmodule_eq_polar`, `nat_card_ofStabilizer_eq`, `SemigroupIdeal.closure_le`, `mem_closure`, `inclusion_injective`, `mem_orbit_subMul_iff`, `val_image_orbit`, `mem_one`, `MulAction.isPreprimitive_fixingSubgroup_insert_iff`, `subtype_apply`, `ofFixingSubgroup_of_eq_apply`, `SemigroupIdeal.mem_closure`, `nat_card_ofStabilizer_eq_add_one`, `SemigroupIdeal.mem_closure_of_mem`, `coe_mul`, `ofFixingSubgroup.isMultiplyPretransitive`, `MultilinearMap.map_nonempty`, `ENat_card_ofStabilizer_add_one_eq`, `notMem_val_image`, `MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup`, `MulAction.isMultiplyPreprimitive_iff`, `mem_ofStabilizer_iff`, `ofStabilizer.snoc_castSucc`, `mem_ofFixingSubgroup_insert_iff`, `Equiv.Perm.isPretransitive_of_isCycle_mem`, `MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `val_smul`, `mem_iInf`, `ofStabilizer.conjMap_comp`, `ofStabilizer.isMultiplyPretransitive`, `ofFixingSubgroup.append_right`, `subset_coe_one`, `subset_closure`, `cosetToCuspOrbit_apply_mk`, `isCentralScalar`, `compl_def`, `coe_one`, `inclusion.coe_eq`, `ofFixingSubgroup_of_singleton_bijective`, `ofFixingSubgroupEmpty_equivariantMap_bijective`, `map_ofFixingSubgroupUnion_bijective`, `ofFixingSubgroup_of_eq_bijective`, `smul_mem_iff'`, `val_neg`, `not_mem_of_mem_ofFixingSubgroup`, `val_preimage_orbit`, `IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter`, `MulAction.isMultiplyPreprimitive_ofStabilizer`, `orbitRel_of_subMul`, `mem_one'`, `smul_mem_iff`, `MulAction.IsBlock.subtype_val_preimage`, `mem_ofFixingSubgroup_iff`, `ofStabilizer.conjMap_bijective`, `isScalarTower`, `ofFixingSubgroup.isMultiplyPretransitive'`, `SemigroupIdeal.coe_closure'`, `val_smul_of_tower`, `neg_mem_iff`, `Submodule.coe_toSubMulAction`, `SemigroupIdeal.mem_closure'`, `ofStabilizer.conjMap_apply`, `isScalarTower'`, `image_inclusion`, `ofFixingSubgroup_insert_map_bijective`, `ext_iff`, `conjMap_ofFixingSubgroup_bijective`, `instSMulMemClass`, `IsPretransitive.isPretransitive_ofFixingSubgroup_inter`, `conjMap_ofFixingSubgroup_coe_apply`, `MulAction.isBlock_subtypeVal`, `coe_pow`
`instSupSet` 📖	CompOp	1 math math: `mem_iSup`
`instTop` 📖	CompOp	—
`instZeroSubtypeMemOfNonempty` 📖	CompOp	—
`mulAction` 📖	CompOp	19 math math: `ofFixingSubgroup_insert_map_apply`, `map_ofFixingSubgroupUnion_def`, `ofStabilizer.isMultiplyPretransitive_iff`, `MulAction.ofFixingSubgroup.isMultiplyPreprimitive`, `stabilizer_of_subMul`, `fixingSubgroup_of_insert`, `ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `stabilizer_of_subMul.submonoid`, `MulAction.isPreprimitive_fixingSubgroup_insert_iff`, `ofFixingSubgroup.isMultiplyPretransitive`, `mem_ofFixingSubgroup_insert_iff`, `MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `ofStabilizer.isMultiplyPretransitive`, `cosetToCuspOrbit_apply_mk`, `map_ofFixingSubgroupUnion_bijective`, `MulAction.isMultiplyPreprimitive_ofStabilizer`, `orbitRel_of_subMul`, `ofFixingSubgroup.isMultiplyPretransitive'`, `ofFixingSubgroup_insert_map_bijective`
`mulAction'` 📖	CompOp	—
`smul'` 📖	CompOp	41 math math: `ofStabilizer.isPretransitive_iff_of_conj`, `MulAction.isPreprimitive_of_fixingSubgroup_empty_iff`, `ofStabilizer.conjMap_comp_apply`, `ofFixingSubgroup_insert_map_apply`, `ofFixingSubgroup_equivariantMap_injective`, `ofStabilizer.conjMap_comp_inv_apply`, `ofFixingSubgroup_of_inclusion_injective`, `ofStabilizer.inv_conjMap_comp_apply`, `map_ofFixingSubgroupUnion_def`, `ofStabilizer.isPretransitive_iff`, `MulAction.isPreprimitive_ofFixingSubgroup_conj_iff`, `inclusion.toFun_eq_coe`, `inclusion_injective`, `mem_orbit_subMul_iff`, `val_image_orbit`, `MulAction.isPreprimitive_fixingSubgroup_insert_iff`, `ofFixingSubgroup_of_eq_apply`, `MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup`, `MulAction.isMultiplyPreprimitive_iff`, `Equiv.Perm.isPretransitive_of_isCycle_mem`, `ofStabilizer.conjMap_comp`, `isCentralScalar`, `inclusion.coe_eq`, `ofFixingSubgroup_of_singleton_bijective`, `ofFixingSubgroupEmpty_equivariantMap_bijective`, `map_ofFixingSubgroupUnion_bijective`, `ofFixingSubgroup_of_eq_bijective`, `val_preimage_orbit`, `IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter`, `MulAction.IsBlock.subtype_val_preimage`, `ofStabilizer.conjMap_bijective`, `isScalarTower`, `val_smul_of_tower`, `ofStabilizer.conjMap_apply`, `isScalarTower'`, `image_inclusion`, `ofFixingSubgroup_insert_map_bijective`, `conjMap_ofFixingSubgroup_bijective`, `IsPretransitive.isPretransitive_ofFixingSubgroup_inter`, `conjMap_ofFixingSubgroup_coe_apply`, `MulAction.isBlock_subtypeVal`
`subtype` 📖	CompOp	3 math math: `subtype_eq_val`, `subtype_injective`, `subtype_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`SetLike.coe` `SubMulAction` `instSetLike`	`copy`	—	—
`compl_def` 📖	mathematical	—	`carrier` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Compl.compl` `SubMulAction` `instCompl` `Set` `Set.instCompl` `SetLike.coe` `instSetLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `SubMulAction` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`SubMulAction` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike`	—	`ext`
`image_inclusion` 📖	mathematical	—	`Set.range` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MulActionHom` `smul'` `Monoid.toMulAction` `IsScalarTower.left` `instFunLikeMulActionHom` `inclusion` `carrier`	—	`IsScalarTower.left` `inclusion.coe_eq` `Subtype.range_coe`
`inclusion_injective` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MulActionHom` `smul'` `Monoid.toMulAction` `IsScalarTower.left` `instFunLikeMulActionHom` `inclusion`	—	`Subtype.val_injective`
`instSMulMemClass` 📖	mathematical	—	`SMulMemClass` `SubMulAction` `instSetLike`	—	`smul_mem'`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `smul'` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `smul_assoc`
`isScalarTower'` 📖	mathematical	—	`IsScalarTower` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `smul'`	—	`smul_assoc`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `SetLike.coe` `SubMulAction` `instSetLike`	—	—
`mem_iInf` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	`Set.iInter_congr_Prop` `Set.iInter_exists` `Set.iInter_iInter_eq'`
`mem_iSup` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike` `iSup` `instSupSet`	—	`Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'`
`mem_orbit_subMul_iff` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership` `MulAction.orbit` `smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `val_preimage_orbit` `Set.mem_preimage`
`neg_mem` 📖	mathematical	`SubMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `instSetLike`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_one_smul` `smul_mem`
`neg_mem_iff` 📖	mathematical	—	`SubMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_neg` `neg_mem`
`orbitRel_of_subMul` 📖	mathematical	—	`MulAction.orbitRel` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `mulAction` `Setoid.comap`	—	`Setoid.ext_iff` `Setoid.comap_rel` `mem_orbit_subMul_iff`
`smul_mem` 📖	—	`SubMulAction` `SetLike.instMembership` `instSetLike`	—	—	`smul_mem'`
`smul_mem'` 📖	—	`Set` `Set.instMembership` `carrier`	—	—	—
`smul_mem_iff` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`smul_mem_iff'` `Units.instIsScalarTower`
`smul_mem_iff'` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`smul_of_tower_mem` `inv_smul_smul`
`smul_of_tower_mem` 📖	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike`	—	—	`one_smul` `smul_assoc` `smul_mem`
`stabilizer_of_subMul` 📖	mathematical	—	`MulAction.stabilizer` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `mulAction`	—	`stabilizer_of_subMul.submonoid`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SubMulAction` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem` `instFunLikeMulActionHom` `subtype`	—	—
`subtype_eq_val` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SubMulAction` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem` `instFunLikeMulActionHom` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MulActionHom` `instSMulSubtypeMem` `instFunLikeMulActionHom` `subtype`	—	`Subtype.coe_injective`
`val_image_orbit` 📖	mathematical	—	`Set.image` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `MulAction.orbit` `smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `Set.range_comp`
`val_neg` 📖	mathematical	—	`SubMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `instSetLike` `instNegSubtypeMem` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`val_preimage_orbit` 📖	mathematical	—	`Set.preimage` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `MulAction.orbit` `smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `val_image_orbit` `Function.Injective.preimage_image` `Subtype.val_injective`
`val_smul` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	—
`val_smul_of_tower` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `smul'`	—	—
`zero_mem` 📖	mathematical	`Set.Nonempty` `SetLike.coe` `SubMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instSetLike`	`SetLike.instMembership`	—	`smul_mem` `zero_smul`

SubMulAction.SMulMemClass

Definitions

Name	Category	Theorems
`subtype` 📖	CompOp	3 math math: `coe_subtype`, `subtype_apply`, `subtype_injective`
`toMulAction` 📖	CompOp	3 math math: `coe_subtype`, `subtype_apply`, `subtype_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SetLike.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `toMulAction` `instFunLikeMulActionHom` `subtype`	—	—
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SetLike.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `toMulAction` `instFunLikeMulActionHom` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `toMulAction` `instFunLikeMulActionHom` `subtype`	—	`Subtype.coe_injective`

SubMulAction.inclusion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `SubMulAction.instSetLike` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left` `instFunLikeMulActionHom` `SubMulAction.inclusion`	—	`IsScalarTower.left`
`toFun_eq_coe` 📖	mathematical	—	`MulActionHom.toFun` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `SubMulAction.instSetLike` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left` `SubMulAction.inclusion`	—	`IsScalarTower.left`

SubMulAction.stabilizer_of_subMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`submonoid` 📖	mathematical	—	`MulAction.stabilizerSubmonoid` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `SubMulAction.instSetLike` `SubMulAction.mulAction`	—	`Submonoid.ext`

Units

Definitions

Name	Category	Theorems
`instMulActionSubtypeNeOfNat` 📖	CompOp	2 math math: `smul_coe`, `orbitRel_nonZero_iff`
`nonZeroSubMul` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orbitRel_nonZero_iff` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MulAction.orbitRel` `Units` `instGroup` `instMulActionSubtypeNeOfNat` `instMulAction` `DistribMulAction.toMulAction`	—	—
`smul_coe` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Units` `SemigroupAction.toSMul` `Monoid.toSemigroup` `instMonoid` `MulAction.toSemigroupAction` `instMulActionSubtypeNeOfNat` `instSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—

VAddMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofVAddAssocClass` 📖	mathematical	—	`VAddMemClass`	—	`vadd_mem` `vadd_zero_vadd`
`vadd_mem` 📖	mathematical	`SetLike.instMembership`	`HVAdd.hVAdd` `instHVAdd`	—	—

(root)

Definitions

Name	Category	Theorems
`SMulMemClass` 📖	CompData	17 math math: `AddSubmonoidClass.nsmulMemClass`, `NonUnitalStarSubalgebra.instSMulMemClass`, `StarSubalgebra.smulMemClass`, `ClosedSubmodule.instSMulMemClass`, `smulMemClass`, `IntermediateField.instSMulMemClass`, `LieSubmodule.instSMulMemClass`, `SMulMemClass.ofIsScalarTower`, `TwoSidedIdeal.instSMulMemClass`, `NonUnitalSubalgebra.instSMulMemClass`, `Subalgebra.instSMulMemClass`, `TwoSidedIdeal.instSMulMemClassMulOpposite`, `Submodule.smulMemClass`, `LieSubalgebra.instSMulMemClass`, `SubMulAction.instSMulMemClass`, `AddSubgroupClass.zsmulMemClass`, `instSMulMemClassHomogeneousSubmodule`
`SubAddAction` 📖	CompData	75 math math: `SubAddAction.map_ofFixingAddSubgroupUnion_bijective`, `SubAddAction.notMem_val_image`, `SubAddAction.subtype_apply`, `SubAddAction.closure_mono`, `SubAddAction.ofStabilizer.conjMap_comp`, `SubAddAction.ofFixingAddSubgroup_of_inclusion_injective`, `SubAddAction.subtype_eq_val`, `SubAddAction.ofFixingAddSubgroup_of_singleton_bijective`, `SubAddAction.mem_ofStabilizer_iff`, `SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff`, `SubAddAction.ofStabilizer.conjMap_comp_neg_apply`, `SubAddAction.instVAddMemClass`, `SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive`, `SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive'`, `SubAddAction.ofStabilizer.isPretransitive_iff`, `SubAddAction.stabilizer_of_subMul.addSubmonoid`, `SubAddAction.conjMap_ofFixingAddSubgroup_bijective`, `SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply`, `SubAddAction.ofFixingAddSubgroup_of_eq_bijective`, `SubAddAction.vaddAssocClass'`, `SubAddAction.subset_closure`, `SubAddAction.val_image_orbit`, `SubAddAction.ofFixingAddSubgroup_insert_map_bijective`, `SubAddAction.nat_card_ofStabilizer_eq`, `SubAddAction.ofFixingAddSubgroup_of_eq_apply`, `SubAddAction.isCentralVAdd`, `SubAddAction.vadd_mem_iff'`, `SubAddAction.ofStabilizer.isMultiplyPretransitive_iff`, `SubAddAction.ofStabilizer.conjMap_bijective`, `SubAddAction.val_preimage_orbit`, `SubAddAction.image_inclusion`, `SubAddAction.mem_iInf`, `SubAddAction.mem_orbit_subAdd_iff`, `SubAddAction.compl_def`, `AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `SubAddAction.ofStabilizer.snoc_castSucc`, `SubAddAction.mem_iSup`, `SubAddAction.ENat_card_ofStabilizer_add_zero_eq`, `SubAddAction.mem_closure`, `SubAddAction.fixingAddSubgroup_of_insert`, `SubAddAction.orbitRel_of_subAdd`, `SubAddAction.mem_ofFixingAddSubgroup_iff`, `SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective`, `SubAddAction.inclusion.coe_eq`, `SubAddAction.ext_iff`, `SubAddAction.ofStabilizer.neg_conjMap_comp_apply`, `SubAddAction.vaddAssocClass`, `AddAction.isMultiplyPreprimitive_iff`, `SubAddAction.mem_carrier`, `SubAddAction.ofFixingAddSubgroup.append_right`, `SubAddAction.ofFixingAddSubgroup_equivariantMap_injective`, `SubAddAction.mem_closure_of_mem`, `SubAddAction.val_vadd`, `AddAction.ofFixingSubgroup.isMultiplyPreprimitive`, `SubAddAction.nat_card_ofStabilizer_add_zero_eq`, `AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup`, `SubAddAction.disjoint_val_image`, `AddAction.IsBlock.subtype_val_preimage`, `SubAddAction.ofStabilizer.conjMap_comp_apply`, `SubAddAction.val_vadd_of_tower`, `SubAddAction.ofStabilizer.isMultiplyPretransitive`, `SubAddAction.inclusion_injective`, `SubAddAction.stabilizer_of_subAdd`, `AddAction.isPreprimitive_fixingAddSubgroup_insert_iff`, `SubAddAction.closure_le`, `AddAction.isMultiplyPreprimitive_ofStabilizer`, `AddAction.isBlock_subtypeVal`, `SubAddAction.mem_ofFixingAddSubgroup_insert_iff`, `AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff`, `SubAddAction.inclusion.toFun_eq_coe`, `SubAddAction.not_mem_of_mem_ofFixingAddSubgroup`, `SubAddAction.ofStabilizer.isPretransitive_iff_of_conj`, `SubAddAction.map_ofFixingAddSubgroupUnion_def`, `SubAddAction.ofStabilizer.conjMap_apply`
`SubMulAction` 📖	CompData	100 math math: `SubMulAction.ofStabilizer.isPretransitive_iff_of_conj`, `MulAction.isPreprimitive_of_fixingSubgroup_empty_iff`, `SubMulAction.ofStabilizer.conjMap_comp_apply`, `SubMulAction.subtype_eq_val`, `SubMulAction.ofFixingSubgroup_equivariantMap_injective`, `SubMulAction.closure_le`, `SubMulAction.ofStabilizer.conjMap_comp_inv_apply`, `SubMulAction.mem_closure_of_mem`, `SubMulAction.ofFixingSubgroup_of_inclusion_injective`, `SubMulAction.subset_coe_pow`, `SubMulAction.nat_card_ofStabilizer_add_one_eq`, `SubMulAction.ofStabilizer.inv_conjMap_comp_apply`, `SubMulAction.mem_iSup`, `SubMulAction.map_ofFixingSubgroupUnion_def`, `SubMulAction.ofStabilizer.isMultiplyPretransitive_iff`, `SubMulAction.subtype_injective`, `MulAction.ofFixingSubgroup.isMultiplyPreprimitive`, `SubMulAction.ofStabilizer.isPretransitive_iff`, `SubMulAction.mem_carrier`, `SubMulAction.stabilizer_of_subMul`, `SubMulAction.mem_mul`, `SubMulAction.fixingSubgroup_of_insert`, `MulAction.isPreprimitive_ofFixingSubgroup_conj_iff`, `SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `SubMulAction.stabilizer_of_subMul.submonoid`, `SubMulAction.inclusion.toFun_eq_coe`, `SubMulAction.disjoint_val_image`, `SubMulAction.algebraMap_mem`, `StrongDual.polarSubmodule_eq_polar`, `SubMulAction.nat_card_ofStabilizer_eq`, `SubMulAction.mem_closure`, `SubMulAction.inclusion_injective`, `SubMulAction.mem_orbit_subMul_iff`, `SubMulAction.val_image_orbit`, `SubMulAction.mem_one`, `MulAction.isPreprimitive_fixingSubgroup_insert_iff`, `SubMulAction.subtype_apply`, `SubMulAction.ofFixingSubgroup_of_eq_apply`, `SubMulAction.nat_card_ofStabilizer_eq_add_one`, `SubMulAction.coe_mul`, `SubMulAction.ofFixingSubgroup.isMultiplyPretransitive`, `MultilinearMap.map_nonempty`, `SubMulAction.ENat_card_ofStabilizer_add_one_eq`, `SubMulAction.notMem_val_image`, `MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup`, `MulAction.isMultiplyPreprimitive_iff`, `SubMulAction.mem_ofStabilizer_iff`, `SubMulAction.ofStabilizer.snoc_castSucc`, `SubMulAction.mem_ofFixingSubgroup_insert_iff`, `Equiv.Perm.isPretransitive_of_isCycle_mem`, `MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer`, `SubMulAction.val_smul`, `SubMulAction.mem_iInf`, `SubMulAction.ofStabilizer.conjMap_comp`, `Submodule.toSubMulAction_strictMono`, `SubMulAction.ofStabilizer.isMultiplyPretransitive`, `SubMulAction.ofFixingSubgroup.append_right`, `SubMulAction.subset_coe_one`, `SubMulAction.subset_closure`, `cosetToCuspOrbit_apply_mk`, `SubMulAction.isCentralScalar`, `SubMulAction.compl_def`, `SubMulAction.coe_one`, `SubMulAction.inclusion.coe_eq`, `SubMulAction.ofFixingSubgroup_of_singleton_bijective`, `SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective`, `SubMulAction.map_ofFixingSubgroupUnion_bijective`, `SubMulAction.ofFixingSubgroup_of_eq_bijective`, `SubMulAction.smul_mem_iff'`, `SubMulAction.val_neg`, `SubMulAction.not_mem_of_mem_ofFixingSubgroup`, `SubMulAction.val_preimage_orbit`, `SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter`, `MulAction.isMultiplyPreprimitive_ofStabilizer`, `SubMulAction.orbitRel_of_subMul`, `SubMulAction.mem_one'`, `SubMulAction.smul_mem_iff`, `MulAction.IsBlock.subtype_val_preimage`, `SubMulAction.mem_ofFixingSubgroup_iff`, `SubMulAction.ofStabilizer.conjMap_bijective`, `SubMulAction.isScalarTower`, `SubMulAction.ofFixingSubgroup.isMultiplyPretransitive'`, `SubMulAction.val_smul_of_tower`, `SubMulAction.neg_mem_iff`, `Submodule.coe_toSubMulAction`, `SubMulAction.closure_mono`, `Submodule.toSubMulAction_one`, `SubMulAction.ofStabilizer.conjMap_apply`, `SubMulAction.isScalarTower'`, `SubMulAction.image_inclusion`, `SubMulAction.ofFixingSubgroup_insert_map_bijective`, `SubMulAction.ext_iff`, `SubMulAction.conjMap_ofFixingSubgroup_bijective`, `Submodule.toSubMulAction_injective`, `SubMulAction.instSMulMemClass`, `Submodule.toSubMulAction_mono`, `SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter`, `SubMulAction.conjMap_ofFixingSubgroup_coe_apply`, `MulAction.isBlock_subtypeVal`, `SubMulAction.coe_pow`
`VAddMemClass` 📖	CompData	2 math math: `SubAddAction.instVAddMemClass`, `VAddMemClass.ofVAddAssocClass`
`fixedPointsSubAddOfNormal` 📖	CompOp	—
`fixedPointsSubMulOfNormal` 📖	CompOp	—
`instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal` 📖	CompOp	3 math math: `MulAction.quotient_out_smul_fixedPoints`, `MulAction.coe_quotient_smul_fixedPoints`, `coe_smul_fixedPoints_of_normal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul_fixedPoints_of_normal` 📖	mathematical	—	`Set` `Set.instMembership` `MulAction.fixedPoints` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.instMulAction` `Set.Elem` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal`	—	—
`smul_mem_fixedPoints_of_normal` 📖	mathematical	`Set` `Set.instMembership` `MulAction.fixedPoints` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.instMulAction`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Subgroup.smul_def` `inv_smul_eq_iff` `smul_smul` `Subgroup.Normal.conj_mem'`
`vadd_mem_fixedPoints_of_normal` 📖	mathematical	`Set` `Set.instMembership` `AddAction.fixedPoints` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.instAddAction`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`AddSubgroup.vadd_def` `neg_vadd_eq_iff` `vadd_vadd` `AddSubgroup.Normal.conj_mem'`

---

← Back to Index