Structures · Algebra
AddAction.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_vadd_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- AddOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- AddAction.exists_vadd_eq
- AddAction.IsPretransitive.exists_vadd_eq
- AddAction.IsBlock.ncard_block_add_ncard_orbit_eq
- AddAction.surjective_vadd
- SubAddAction.ofStabilizer.isMultiplyPretransitive
- AddAction.IsPretransitive.discreteTopology_iff
- AddAction.IsPretransitive.of_vadd_eq
- AddAction.index_stabilizer_of_transitive
- AddAction.IsPreprimitive.of_isTrivialBlock_base
- SubAddAction.exists_vadd_of_last_eq
- AddAction.IsBlock.eq_univ_of_card_lt
- AddAction.IsBlock.of_subset
- isOpenMap_vadd_of_sigmaCompact
- AddAction.isSimpleOrder_blockMem_iff_isPreprimitive
- AddAction.orbit_eq_univ
- AddAction.isCoatom_stabilizer_iff_preprimitive
- AddAction.IsBlock.ncard_dvd_card
- AddAction.isMultiplyPreprimitive_ofStabilizer
- AddAction.IsBlock.isBlockSystem
- AddAction.isPretransitive_compHom
- AddAction.IsBlock.orbit_stabilizer_eq
- AddAction.IsPretransitive.t1Space_iff
- AddAction.IsPretransitive.of_embedding
- AddAction.block_stabilizerOrderIso
- vadd_singleton_mem_nhds_of_sigmaCompact
- AddAction.IsBlock.ncard_block_eq_relIndex
- AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer
- AddAction.IsPretransitive.of_compHom
- AddAction.IsPretransitive.of_vaddAssocClass
- AddAction.properVAdd_of_proper_orbitMap
- AddAction.equivAddSubgroupOrbitsQuotientAddGroup
- SubAddAction.ofStabilizer.isPretransitive_iff
- AddAction.IsPreprimitive.of_card_lt
- AddAction.finite_quotient_of_pretransitive_of_finite_quotient
- Multiplicative.mulAction_isPretransitive
- SubAddAction.ofStabilizer.isMultiplyPretransitive_iff
- AddAction.IsBlock.subsingleton_of_card_lt
- SeparationQuotient.instIsPretransitiveVAdd
- AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero
- AddAction.IsPreprimitive.of_prime_card
- AddAction.isMinimal_of_pretransitive
Ancestors0
No ancestors.