Mathlib Map

Theorems · Definition · group theory

AddAction.IsFixedBlock

(G : Type u_1) → {X : Type u_2} → [VAdd G X] → Set X → Prop

A set B is a G-fixed block if g +ᵥ B = B for all g : G.

Defined in
Mathlib.GroupTheory.GroupAction.Blocks
Cited by
6 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
VAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddAction.IsFixedBlock.isBlock · cited by 3IsFixedBlock.isBlockAddAction.IsInvariantBlock.isFixedBlock · cited by 1IsInvariantBlock.isFixedB…AddAction.isInvariantBlock_iff_isFixedBlock · cited by 1AddAction.isInvariantBloc…AddAction.IsFixedBlock.isInvariantBlock · cited by 1IsFixedBlock.isInvariantB…AddAction.IsFixedBlock.orbit · cited by 1IsFixedBlock.orbitAddAction.IsFixedBlock.univ · cited by 1IsFixedBlock.univSet · cited by 53352SetHVAdd.hVAdd · cited by 1820HVAdd.hVAddVAdd · cited by 616VAddAddAction.IsFixedBlockCITED BYCITES

Cites3

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
  • HVAdd.hVAddproof · cited by 1,820
  • VAddstatement and proof · cited by 616

Cited by6

Results whose statement or proof uses this declaration.