Theorems · Theorem · group theory

AddAction.minimalPeriod_eq_card

∀ {α : Type u_3} {β : Type u_4} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β)
  [inst_2 : Fintype ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)],
  Function.minimalPeriod (fun x => a +ᵥ x) b = Fintype.card ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)

Defined in: Mathlib.Data.ZMod.QuotientGroup
Cited by: 0 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup AddAction Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
AddGroupstatement and proof · cited by 4,410
AddSubgroupstatement · cited by 3,232
HVAdd.hVAddstatement and proof · cited by 1,820
Fintype.cardstatement · cited by 1,386
AddActionstatement and proof · cited by 820
AddSubgroup.zmultiplesstatement and proof · cited by 493
Function.minimalPeriodstatement and proof · cited by 100
AddAction.orbitstatement and proof · cited by 86
ZMod.cardproof · cited by 36
Fintype.ofEquiv_cardproof · cited by 16

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.