Theorems · Theorem · group theory

AddAction.IsBlock.ncard_block_eq_relIndex

∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  {B : Set X},
  AddAction.IsBlock G B → ∀ {x : X}, x ∈ B → B.ncard = (AddAction.stabilizer G x).relIndex (AddAction.stabilizer G B)

Defined in: Mathlib.GroupTheory.GroupAction.Blocks
Cited by: 1 results in Mathlib
Foundations: Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup AddAction AddAction.IsPretransitive

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites15

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
AddGroupstatement and proof · cited by 4,410
AddSubgroupproof · cited by 3,232
AddActionstatement and proof · cited by 820
Set.ncardstatement and proof · cited by 344
AddAction.stabilizerstatement and proof · cited by 112
AddSubgroup.indexproof · cited by 104
AddSubgroup.addSubgroupOfproof · cited by 87
AddSubgroup.extproof · cited by 75
AddSubgroup.relIndexstatement · cited by 67
AddAction.IsBlockstatement and proof · cited by 65
AddAction.IsPretransitivestatement and proof · cited by 56

Cited by1

Results whose statement or proof uses this declaration.

AddAction.IsBlock.ncard_block_add_ncard_orbit_eqproof · cited by 4