MultiplePrimitivity

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

Statistics

Metric	Count
Definitions IsMultiplyPreprimitive, IsMultiplyPreprimitive	2
Theorems isMultiplyPretransitive, isPreprimitive_ofFixingAddSubgroup, of_bijective_map, instIsMultiplyPretransitiveOfIsMultiplyPreprimitive, isMultiplyPreprimitive_congr, isMultiplyPreprimitive_iff, isMultiplyPreprimitive_ofStabilizer, isMultiplyPreprimitive_of_isMultiplyPretransitive_succ, isMultiplyPreprimitive_of_le, isMultiplyPreprimitive_succ_iff_ofStabilizer, isPreprimitive_fixingAddSubgroup_insert_iff, isPreprimitive_ofFixingAddSubgroup_addConj_iff, isPreprimitive_of_fixingAddSubgroup_empty_iff, is_zero_preprimitive, is_zero_preprimitive_iff, isMultiplyPreprimitive, isMultiplyPretransitive, isPreprimitive_ofFixingSubgroup, of_bijective_map, instIsMultiplyPretransitiveOfIsMultiplyPreprimitive, isMultiplyPreprimitive_congr, isMultiplyPreprimitive_iff, isMultiplyPreprimitive_ofStabilizer, isMultiplyPreprimitive_of_isMultiplyPretransitive_succ, isMultiplyPreprimitive_of_le, isMultiplyPreprimitive_succ_iff_ofStabilizer, isPreprimitive_fixingSubgroup_insert_iff, isPreprimitive_ofFixingSubgroup_conj_iff, isPreprimitive_of_fixingSubgroup_empty_iff, is_one_preprimitive_iff, is_zero_preprimitive, isMultiplyPreprimitive	32
Total	34

AddAction

Definitions

Name	Category	Theorems
IsMultiplyPreprimitive 📖	CompData	10 math math: is_zero_preprimitive, isMultiplyPreprimitive_of_le, isMultiplyPreprimitive_of_isMultiplyPretransitive_succ, isMultiplyPreprimitive_congr, isMultiplyPreprimitive_succ_iff_ofStabilizer, IsMultiplyPreprimitive.of_bijective_map, is_zero_preprimitive_iff, isMultiplyPreprimitive_iff, ofFixingSubgroup.isMultiplyPreprimitive, isMultiplyPreprimitive_ofStabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMultiplyPretransitiveOfIsMultiplyPreprimitive 📖	mathematical	—	IsMultiplyPretransitive	—	IsMultiplyPreprimitive.isMultiplyPretransitive
isMultiplyPreprimitive_congr 📖	mathematical	Function.Bijective DFunLike.coe AddActionHom AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction instFunLikeAddActionHom	IsMultiplyPreprimitive	—	IsMultiplyPreprimitive.of_bijective_map VAddAssocClass.left isMultiplyPreprimitive_iff IsPretransitive.of_embedding_congr IsMultiplyPreprimitive.isMultiplyPretransitive mem_fixingAddSubgroup_iff Function.Bijective.surjective Set.mem_image AddActionSemiHomClass.map_vaddₛₗ instAddActionSemiHomClassAddActionHom SubAddAction.mem_ofFixingAddSubgroup_iff Function.Bijective.injective Subtype.prop VAddMemClass.vadd_mem SubAddAction.instVAddMemClass isPreprimitive_congr Set.mem_image_of_mem IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup Set.InjOn.encard_image Function.Injective.injOn
isMultiplyPreprimitive_iff 📖	mathematical	—	IsMultiplyPreprimitive IsMultiplyPretransitive IsPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left	—	VAddAssocClass.left
isMultiplyPreprimitive_ofStabilizer 📖	mathematical	—	IsMultiplyPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.addAction	—	is_zero_preprimitive VAddAssocClass.left isMultiplyPreprimitive_iff SubAddAction.ofStabilizer.isMultiplyPretransitive IsMultiplyPreprimitive.isMultiplyPretransitive IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup Set.encard_insert_of_notMem Set.mem_image Set.mem_singleton_iff Function.Injective.encard_image Subtype.coe_injective Nat.cast_succ IsPreprimitive.of_surjective Function.Bijective.surjective AddSubgroup.instVAddAssocClassSubtypeMem SubAddAction.vaddAssocClass' SubAddAction.ofFixingAddSubgroup_insert_map_bijective
isMultiplyPreprimitive_of_isMultiplyPretransitive_succ 📖	mathematical	ENat instLEENat ENat.instNatCast ENat.card	IsMultiplyPreprimitive	—	is_zero_preprimitive VAddAssocClass.left isMultiplyPreprimitive_iff isMultiplyPretransitive_of_le' isPreprimitive_of_is_two_pretransitive ENat.add_left_injective_of_ne_top ENat.one_ne_top zero_add add_comm Nat.cast_add Nat.cast_one Set.finite_of_encard_eq_coe SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive
isMultiplyPreprimitive_of_le 📖	mathematical	ENat instLEENat ENat.instNatCast ENat.card	IsMultiplyPreprimitive	—	isMultiplyPreprimitive_of_isMultiplyPretransitive_succ instIsMultiplyPretransitiveOfIsMultiplyPreprimitive le_trans ENat.coe_le_coe
isMultiplyPreprimitive_succ_iff_ofStabilizer 📖	mathematical	—	IsMultiplyPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.addAction	—	isMultiplyPreprimitive_ofStabilizer VAddAssocClass.left isMultiplyPreprimitive_iff SubAddAction.ofStabilizer.isMultiplyPretransitive IsMultiplyPreprimitive.isMultiplyPretransitive Set.nonempty_def Set.nonempty_iff_ne_empty not_lt Nat.cast_one zero_add Set.encard_empty zero_lt_one Nat.instZeroLEOneClass exists_vadd_eq isPreprimitive_ofFixingAddSubgroup_addConj_iff Set.ext Set.mem_insert_iff Set.mem_image Set.mem_insert_of_mem Set.mem_preimage Set.vadd_mem_vadd_set_iff AddSubgroup.instVAddAssocClassSubtypeMem SubAddAction.vaddAssocClass' isPreprimitive_fixingAddSubgroup_insert_iff IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup ENat.add_left_injective_of_ne_top ENat.one_ne_top Nat.cast_add neg_vadd_vadd Set.image_vadd Function.Injective.encard_image injective Set.encard_insert_of_notMem SubAddAction.notMem_val_image Subtype.coe_injective ENat.coe_one
isPreprimitive_fixingAddSubgroup_insert_iff 📖	mathematical	—	IsPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instInsert Set.image SubAddAction stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.ofFixingAddSubgroup SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left SubAddAction.addAction AddSubgroup.instVAddAssocClassSubtypeMem SubAddAction.vaddAssocClass'	—	isPreprimitive_congr AddEquiv.surjective SubAddAction.ofFixingAddSubgroup_insert_map_bijective
isPreprimitive_ofFixingAddSubgroup_addConj_iff 📖	mathematical	—	IsPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left HVAdd.hVAdd Set instHVAdd Set.vaddSet	—	isPreprimitive_congr AddEquiv.surjective SubAddAction.addConjMap_ofFixingAddSubgroup_bijective
isPreprimitive_of_fixingAddSubgroup_empty_iff 📖	mathematical	—	IsPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instEmptyCollection SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left	—	isPreprimitive_congr SubAddAction.of_fixingAddSubgroupEmpty_mapScalars_surjective SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective
is_zero_preprimitive 📖	mathematical	—	IsMultiplyPreprimitive	—	is_zero_pretransitive Fin.isEmpty' VAddAssocClass.left CharP.cast_eq_zero CharP.ofCharZero add_eq_zero Unique.instSubsingleton Set.encard_eq_zero one_ne_zero NeZero.charZero_one
is_zero_preprimitive_iff 📖	mathematical	—	IsMultiplyPreprimitive IsPreprimitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	—	VAddAssocClass.left isPreprimitive_of_fixingAddSubgroup_empty_iff IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup Set.encard_empty zero_add Nat.cast_one isMultiplyPreprimitive_iff is_zero_pretransitive_iff IsPreprimitive.toIsPretransitive IsAddRightRegular.add_right_eq_self_iff isAddRightRegular_iff_isAddRegular IsAddRegular.of_ne_top ENat.one_ne_top Set.encard_eq_zero

AddAction.IsMultiplyPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMultiplyPretransitive 📖	mathematical	—	AddAction.IsMultiplyPretransitive	—	—
isPreprimitive_ofFixingAddSubgroup 📖	mathematical	ENat instAddENat Set.encard AddMonoidWithOne.toOne instAddMonoidWithOneENat ENat.instNatCast	AddAction.IsPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left	—	—
of_bijective_map 📖	mathematical	Function.Bijective DFunLike.coe AddActionHom AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instFunLikeAddActionHom	AddAction.IsMultiplyPreprimitive	—	AddAction.IsPretransitive.of_embedding Function.Bijective.surjective AddAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive Set.image_preimage_eq Set.mem_image AddActionSemiHomClass.map_vaddₛₗ instAddActionSemiHomClassAddActionHom mem_fixingAddSubgroup_iff VAddAssocClass.left Set.mem_preimage SetLike.coe_eq_coe AddActionHom.map_vadd' isPreprimitive_ofFixingAddSubgroup Function.Injective.encard_image Function.Bijective.injective AddAction.IsPreprimitive.of_surjective

AddAction.ofFixingSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMultiplyPreprimitive 📖	mathematical	Set.ncard	AddAction.IsMultiplyPreprimitive AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup SubAddAction AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup SubAddAction.addAction	—	SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive AddAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive Set.preimage_image_eq Subtype.coe_injective VAddAssocClass.left AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup Set.encard_union_eq SubAddAction.disjoint_val_image Function.Injective.encard_image add_assoc Nat.cast_add Set.Finite.cast_ncard_eq Set.toFinite AddAction.IsPreprimitive.of_surjective Function.Bijective.surjective AddSubgroup.instVAddAssocClassSubtypeMem SubAddAction.vaddAssocClass' SubAddAction.map_ofFixingAddSubgroupUnion_bijective

MulAction

Definitions

Name	Category	Theorems
IsMultiplyPreprimitive 📖	CompData	13 math math: is_zero_preprimitive, is_one_preprimitive_iff, ofFixingSubgroup.isMultiplyPreprimitive, isMultiplyPreprimitive_congr, IsPreprimitive.is_two_preprimitive, isMultiplyPreprimitive_of_isMultiplyPretransitive_succ, isMultiplyPreprimitive_of_le, isMultiplyPreprimitive_iff, isMultiplyPreprimitive_succ_iff_ofStabilizer, IsMultiplyPreprimitive.of_bijective_map, IsPreprimitive.is_two_motive_of_is_motive, IsPreprimitive.isMultiplyPreprimitive, isMultiplyPreprimitive_ofStabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMultiplyPretransitiveOfIsMultiplyPreprimitive 📖	mathematical	—	IsMultiplyPretransitive	—	IsMultiplyPreprimitive.isMultiplyPretransitive
isMultiplyPreprimitive_congr 📖	mathematical	Function.Bijective DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction instFunLikeMulActionHom	IsMultiplyPreprimitive	—	IsMultiplyPreprimitive.of_bijective_map IsScalarTower.left isMultiplyPreprimitive_iff IsPretransitive.of_embedding_congr IsMultiplyPreprimitive.isMultiplyPretransitive Function.Bijective.surjective MulActionSemiHomClass.map_smulₛₗ instMulActionSemiHomClassMulActionHom Function.Bijective.injective Subtype.prop SMulMemClass.smul_mem SubMulAction.instSMulMemClass isPreprimitive_congr Set.mem_image_of_mem IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup Set.InjOn.encard_image Function.Injective.injOn
isMultiplyPreprimitive_iff 📖	mathematical	—	IsMultiplyPreprimitive IsMultiplyPretransitive IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left	—	IsScalarTower.left
isMultiplyPreprimitive_ofStabilizer 📖	mathematical	—	IsMultiplyPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.mulAction	—	is_zero_preprimitive IsScalarTower.left isMultiplyPreprimitive_iff SubMulAction.ofStabilizer.isMultiplyPretransitive IsMultiplyPreprimitive.isMultiplyPretransitive IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup Set.encard_insert_of_notMem Function.Injective.encard_image Subtype.coe_injective Nat.cast_succ IsPreprimitive.of_surjective Function.Bijective.surjective Subgroup.instIsScalarTowerSubtypeMem SubMulAction.isScalarTower' SubMulAction.ofFixingSubgroup_insert_map_bijective
isMultiplyPreprimitive_of_isMultiplyPretransitive_succ 📖	mathematical	ENat instLEENat ENat.instNatCast ENat.card	IsMultiplyPreprimitive	—	is_zero_preprimitive IsScalarTower.left isMultiplyPreprimitive_iff isMultiplyPretransitive_of_le' isPreprimitive_of_is_two_pretransitive ENat.add_left_injective_of_ne_top ENat.one_ne_top zero_add add_comm Nat.cast_add Nat.cast_one Set.finite_of_encard_eq_coe SubMulAction.ofFixingSubgroup.isMultiplyPretransitive
isMultiplyPreprimitive_of_le 📖	mathematical	ENat instLEENat ENat.instNatCast ENat.card	IsMultiplyPreprimitive	—	isMultiplyPreprimitive_of_isMultiplyPretransitive_succ instIsMultiplyPretransitiveOfIsMultiplyPreprimitive le_trans ENat.coe_le_coe
isMultiplyPreprimitive_succ_iff_ofStabilizer 📖	mathematical	—	IsMultiplyPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.mulAction	—	isMultiplyPreprimitive_ofStabilizer IsScalarTower.left isMultiplyPreprimitive_iff SubMulAction.ofStabilizer.isMultiplyPretransitive IsMultiplyPreprimitive.isMultiplyPretransitive Set.nonempty_def Set.nonempty_iff_ne_empty not_lt Nat.cast_one zero_add Set.encard_empty Nat.instZeroLEOneClass exists_smul_eq isPreprimitive_ofFixingSubgroup_conj_iff Set.ext Set.mem_insert_of_mem Set.mem_insert_iff Subgroup.instIsScalarTowerSubtypeMem SubMulAction.isScalarTower' isPreprimitive_fixingSubgroup_insert_iff IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup ENat.add_left_injective_of_ne_top ENat.one_ne_top Nat.cast_add inv_smul_smul Set.image_smul Function.Injective.encard_image injective Set.encard_insert_of_notMem SubMulAction.notMem_val_image Subtype.coe_injective ENat.coe_one
isPreprimitive_fixingSubgroup_insert_iff 📖	mathematical	—	IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInsert Set.image SubMulAction stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left SubMulAction.mulAction Subgroup.instIsScalarTowerSubtypeMem SubMulAction.isScalarTower'	—	isPreprimitive_congr MulEquiv.surjective SubMulAction.ofFixingSubgroup_insert_map_bijective
isPreprimitive_ofFixingSubgroup_conj_iff 📖	mathematical	—	IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left Set Set.smulSet	—	isPreprimitive_congr MulEquiv.surjective SubMulAction.conjMap_ofFixingSubgroup_bijective
isPreprimitive_of_fixingSubgroup_empty_iff 📖	mathematical	—	IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instEmptyCollection SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left	—	isPreprimitive_congr SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
is_one_preprimitive_iff 📖	mathematical	—	IsMultiplyPreprimitive IsPreprimitive SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	—	IsScalarTower.left isPreprimitive_of_fixingSubgroup_empty_iff IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup Set.encard_empty zero_add Nat.cast_one isMultiplyPreprimitive_iff is_one_pretransitive_iff IsPreprimitive.toIsPretransitive
is_zero_preprimitive 📖	mathematical	—	IsMultiplyPreprimitive	—	is_zero_pretransitive Fin.isEmpty' IsScalarTower.left CharP.cast_eq_zero CharP.ofCharZero Unique.instSubsingleton NeZero.charZero_one

MulAction.IsMultiplyPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMultiplyPretransitive 📖	mathematical	—	MulAction.IsMultiplyPretransitive	—	—
isPreprimitive_ofFixingSubgroup 📖	mathematical	ENat instAddENat Set.encard AddMonoidWithOne.toOne instAddMonoidWithOneENat ENat.instNatCast	MulAction.IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left	—	—
of_bijective_map 📖	mathematical	Function.Bijective DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instFunLikeMulActionHom	MulAction.IsMultiplyPreprimitive	—	MulAction.IsPretransitive.of_embedding Function.Bijective.surjective MulAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive Set.image_preimage_eq Set.mem_image MulActionSemiHomClass.map_smulₛₗ instMulActionSemiHomClassMulActionHom mem_fixingSubgroup_iff IsScalarTower.left Set.mem_preimage SetLike.coe_eq_coe MulActionHom.map_smul' isPreprimitive_ofFixingSubgroup Function.Injective.encard_image Function.Bijective.injective MulAction.IsPreprimitive.of_surjective

MulAction.ofFixingSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMultiplyPreprimitive 📖	mathematical	Set.ncard	MulAction.IsMultiplyPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SubMulAction SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.mulAction	—	SubMulAction.ofFixingSubgroup.isMultiplyPretransitive MulAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive Set.preimage_image_eq Subtype.coe_injective IsScalarTower.left MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup Set.encard_union_eq SubMulAction.disjoint_val_image Function.Injective.encard_image add_assoc Nat.cast_add Set.Finite.cast_ncard_eq Set.toFinite MulAction.IsPreprimitive.of_surjective Function.Bijective.surjective Subgroup.instIsScalarTowerSubtypeMem SubMulAction.isScalarTower' SubMulAction.map_ofFixingSubgroupUnion_bijective

---

← Back to Index