Structures · Algebra
MulAction.IsPreprimitive
An action is preprimitive if it is pretransitive and the only blocks are the trivial ones
- Shape
- 2 explicit arguments · adds isTrivialBlock_of_isBlock
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Matrix.SpecialLinearGroup
- Equiv.Perm
- SpecialLinearGroup
- Matrix.ProjectiveSpecialLinearGroup
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
- MulAction.IsPreprimitive.of_surjective
- MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset
- alternatingGroup.subgroup_eq_top_of_isPreprimitive
- MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul
- MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive
- MulAction.isPreprimitive_stabilizer_subgroup
- MulAction.IsPreprimitive.of_card_lt
- MulAction.IsPreprimitive.isQuasiPreprimitive
- MulAction.IsPreprimitive.toIsPretransitive
- MulAction.IsBlock.subsingleton_or_eq_univ
- Equiv.Perm.alternatingGroup_le_of_isPreprimitive