Mathlib Map

Theorems · Definition · group theory

MulAction.IsFixedBlock

(G : Type u_1) → {X : Type u_2} → [SMul 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
SMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MulAction.IsFixedBlock.isBlock · cited by 3IsFixedBlock.isBlockMulAction.IsInvariantBlock.isFixedBlock · cited by 1IsInvariantBlock.isFixedB…MulAction.isInvariantBlock_iff_isFixedBlock · cited by 1MulAction.isInvariantBloc…MulAction.IsFixedBlock.isInvariantBlock · cited by 1IsFixedBlock.isInvariantB…MulAction.IsFixedBlock.orbit · cited by 1IsFixedBlock.orbitMulAction.IsFixedBlock.univ · cited by 1IsFixedBlock.univSet · cited by 53352SetMulAction.IsFixedBlockCITED BYCITES

Cites1

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

Cited by6

Results whose statement or proof uses this declaration.