Structures · Algebra
AddAction.IsPreprimitive
An additive 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 instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- AddAction.IsPreprimitive.isTrivialBlock_of_isBlock
- AddAction.IsPreprimitive.of_surjective
- AddAction.IsPreprimitive.exists_mem_vadd_and_notMem_vadd
- AddAction.IsPreprimitive.toIsPretransitive
- AddAction.IsBlock.subsingleton_or_eq_univ
- AddAction.IsPreprimitive.of_card_lt
- AddAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive
- AddAction.IsPreprimitive.isQuasiPreprimitive