Theorems · Theorem · group theory

IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf

∀ {G : Type u_1} [inst : AddMonoid G] {x y : G} [inst_1 : DecidableEq G],
  IsOfFinAddOrder x →
    (y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x)))

Defined in: Mathlib.GroupTheory.OrderOfElement
Cited by: 2 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddMonoid DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

Finsetstatement · cited by 13,712
AddMonoidstatement and proof · cited by 2,864
Finset.rangestatement · cited by 1,341
AddSubmonoidstatement · cited by 1,178
Finset.imagestatement · cited by 910
addOrderOfstatement · cited by 208
IsOfFinAddOrderstatement and proof · cited by 105
AddSubmonoid.multiplesstatement · cited by 40
IsOfFinAddOrder.addOrderOf_posproof · cited by 16
mod_addOrderOf_nsmulproof · cited by 7
Finset.mem_range_iff_mem_finset_range_of_mod_eq'proof · cited by 4

Cited by2

Results whose statement or proof uses this declaration.

IsOfFinAddOrder.multiples_eq_image_range_addOrderOfproof · cited by 2
IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOfproof · cited by 1