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_conj_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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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_conj_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_conj_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.conjMap_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 Set.encard_eq_zero top_add ENat.top_ne_one ENat.ne_top_iff_exists ENat.coe_add CharP.cast_eq_zero CharP.ofCharZero

AddAction.IsMultiplyPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMultiplyPretransitive 📖	mathematical	—	AddAction.IsMultiplyPretransitive	—	—
isPreprimitive_ofFixingAddSubgroup 📖	mathematical	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set.encard AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Set.encard_eq_zero top_add ENat.ne_top_iff_exists ENat.coe_add CharP.cast_eq_zero CharP.ofCharZero
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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set.encard AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne 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