Structures · Algebra
MulAction.IsPretransitive
M acts pretransitively on α if for any x y there is g such that g • x = y.
A transitive action should furthermore have α nonempty.
- Shape
- 2 explicit arguments · adds exists_smul_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances7
- Matrix.SpecialLinearGroup
- Equiv.Perm
- CategoryTheory.Aut
- Matrix.ProjGenLinGroup
- Matrix.GeneralLinearGroup
- MulOpposite
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- MulAction.exists_smul_eq
- MulAction.IsPretransitive.exists_smul_eq
- SubMulAction.ofStabilizer.isMultiplyPretransitive
- MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq
- MulAction.isCoatom_stabilizer_iff_preprimitive
- MulAction.IsBlock.eq_univ_of_card_lt
- MulAction.IsPreprimitive.of_prime_card
- surjective_of_isSwap_of_isPretransitive'
- MulAction.IsPretransitive.discreteTopology_iff
- MulAction.index_stabilizer_of_transitive
- MulAction.orbit_eq_univ
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois
- MulAction.surjective_smul
- MulAction.IsPretransitive.of_smul_eq
- MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer
- MulAction.IsPretransitive.of_compHom
- closure_of_isSwap_of_isPretransitive
- MulAction.isSimpleOrder_blockMem_iff_isPreprimitive
- smul_singleton_mem_nhds_of_sigmaCompact
- isOpenMap_smul_of_sigmaCompact
- MulAction.block_stabilizerOrderIso
- MulAction.IsPretransitive.t1Space_iff
- MulAction.IsPreprimitive.of_isTrivialBlock_base
- MulAction.IsBlock.of_subset
- MulAction.IsBlock.orbit_stabilizer_eq
- SubMulAction.exists_smul_of_last_eq
- MulAction.isPretransitive_compHom
- MulAction.IsBlock.isBlockSystem
- MulAction.IsBlock.ncard_dvd_card
- MulAction.IsPretransitive.of_embedding
- MulAction.IsBlock.ncard_block_eq_relIndex
- CategoryTheory.FintypeCat.Action.isConnected_of_transitive
- MulAction.isMultiplyPreprimitive_ofStabilizer
- MulAction.IsPreprimitive.of_card_lt
- MulAction.equivSubgroupOrbitsQuotientGroup
- MulAction.properSMul_of_proper_orbitMap
- Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top
- SubMulAction.ofStabilizer.isMultiplyPretransitive_iff
- SubMulAction.ofStabilizer.isPretransitive_iff
- Additive.addAction_isPretransitive
- CategoryTheory.ActionCategory.instIsConnectedOfIsPretransitiveOfNonempty
- MulAction.isMinimal_of_pretransitive
- SeparationQuotient.instIsPretransitiveSMul
- MulAction.finite_quotient_of_pretransitive_of_finite_quotient
- Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero
- MulAction.IsBlock.subsingleton_of_card_lt
- MulAction.IsPretransitive.of_isScalarTower
- surjective_of_isSwap_of_isPretransitive
Ancestors0
No ancestors.