Theorems · Definition · group theory
AddAction.IsBlock
(G : Type u_1) → {X : Type u_2} → [VAdd G X] → Set X → PropA set B is a G-block iff the sets of the form g +ᵥ B are pairwise equal or disjoint.
- Defined in
- Mathlib.GroupTheory.GroupAction.Blocks
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- VAdd
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Disjointproof · cited by 2,201
- HVAdd.hVAddproof · cited by 1,820
- VAddstatement and proof · cited by 616
Cited by70
Results whose statement or proof uses this declaration.
- AddAction.IsPreprimitive.isTrivialBlock_of_isBlockstatement · cited by 6
- AddAction.IsPreprimitive.of_surjectiveproof · cited by 4
- AddAction.isBlock_iff_vadd_eq_of_nonemptystatement · cited by 4
- AddAction.isPreprimitive_congrproof · cited by 4
- AddAction.BlockMemproof · cited by 4
- AddAction.IsBlock.ncard_block_add_ncard_orbit_eqstatement and proof · cited by 4
- AddAction.IsBlock.translatestatement and proof · cited by 4
- AddAction.isBlock_iff_disjoint_vadd_of_nestatement and proof · cited by 3
- AddAction.isBlock_iff_vadd_eq_or_disjointstatement · cited by 3
- AddAction.isBlock_iff_vadd_eq_vadd_of_nonemptystatement · cited by 3
- AddAction.IsBlock.preimagestatement and proof · cited by 3
- AddAction.IsFixedBlock.isBlockstatement · cited by 3