Theorems · Inductive type · group theory
AddAction.IsMultiplyPreprimitive
(M : Type u_1) → (α : Type u_2) → [inst : AddGroup M] → [AddAction M α] → ℕ → Prop
An additive action is n-multiply preprimitive if it is n-multiply pretransitive
and if, when n ≥ 1, for every set s of cardinality n - 1,
the action of fixingAddSubgroup M s on the complement of s is preprimitive.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by14
Results whose statement or proof uses this declaration.
- AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroupstatement and proof · cited by 6
- AddAction.isMultiplyPreprimitive_iffstatement and proof · cited by 5
- AddAction.IsMultiplyPreprimitive.isMultiplyPretransitivestatement and proof · cited by 3
- AddAction.is_zero_preprimitivestatement · cited by 2
- AddAction.isMultiplyPreprimitive_ofStabilizerstatement and proof · cited by 1
- AddAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succstatement and proof · cited by 1
- AddAction.IsMultiplyPreprimitive.casesOnstatement and proof · cited by 1
- AddAction.IsMultiplyPreprimitive.of_bijective_mapstatement and proof · cited by 1
- AddAction.is_zero_preprimitive_iffstatement and proof · cited by 0
- AddAction.isMultiplyPreprimitive_congrstatement and proof · cited by 0
- AddAction.isMultiplyPreprimitive_of_lestatement and proof · cited by 0
- AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizerstatement and proof · cited by 0