ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>a : G<VAR>ha : IsOfFinAddOrder a<GOAL>(↑(AddSubmonoid.multiples a)).Finite
<VAR>G : Type u_1<VAR>Monoid G<VAR>a : G<VAR>ha : IsOfFinOrder a<GOAL>(↑(Submonoid.powers a)).Finite
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<GOAL>orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<GOAL>addOrderOf (x + y) ∣ (addOrderOf x).lcm (addOrderOf y)
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<GOAL>orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<GOAL>addOrderOf y ∣ (addOrderOf x).lcm (addOrderOf (x + y))
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<GOAL>orderOf (x * y) ∣ orderOf x * orderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<GOAL>addOrderOf (x + y) ∣ addOrderOf x * addOrderOf y
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hco : (orderOf x).Coprime (orderOf y)<GOAL>orderOf (x * y) = orderOf x * orderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<VAR>hco : (addOrderOf x).Coprime (addOrderOf y)<GOAL>addOrderOf (x + y) = addOrderOf x * addOrderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<VAR>hx : IsOfFinAddOrder x<VAR>hy : IsOfFinAddOrder y<GOAL>IsOfFinAddOrder (x + y)
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : IsOfFinOrder x<VAR>hy : IsOfFinOrder y<GOAL>IsOfFinOrder (x * y)
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<GOAL>orderOf (x * y) = orderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<VAR>hy : IsOfFinAddOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y<GOAL>addOrderOf (x + y) = addOrderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hg : p • x = 0<VAR>hg1 : x ≠ 0<GOAL>addOrderOf x = p
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hg : x ^ p = 1<VAR>hg1 : x ≠ 1<GOAL>orderOf x = p
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnot : ¬p ^ n • x = 0<VAR>hfin : p ^ (n + 1) • x = 0<GOAL>addOrderOf x = p ^ (n + 1)
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnot : ¬x ^ p ^ n = 1<VAR>hfin : x ^ p ^ (n + 1) = 1<GOAL>orderOf x = p ^ (n + 1)
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(∃ k, addOrderOf x = p ^ k) ↔ ∃ m, p ^ m • x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(∃ k, orderOf x = p ^ k) ↔ ∃ m, x ^ p ^ m = 1
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>m n : ℕ<GOAL>x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>m n : ℕ<GOAL>n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<GOAL>(Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<GOAL>(Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>n m : ℕ<GOAL>x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>n m : ℕ<GOAL>n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>h : addOrderOf x = 0<VAR>n m : ℕ<GOAL>n • x = m • x ↔ n = m
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>h : orderOf x = 0<VAR>n m : ℕ<GOAL>x ^ n = x ^ m ↔ n = m
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>h : ¬IsOfFinAddOrder x<GOAL>{y | ¬IsOfFinAddOrder y}.Infinite
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>h : ¬IsOfFinOrder x<GOAL>{y | ¬IsOfFinOrder y}.Infinite
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>a : G<GOAL>(↑(Submonoid.powers a)).Finite ↔ IsOfFinOrder a
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>a : G<GOAL>(↑(AddSubmonoid.multiples a)).Finite ↔ IsOfFinAddOrder a
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>a : G<GOAL>(↑(AddSubmonoid.multiples a)).Infinite ↔ ¬IsOfFinAddOrder a
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>a : G<GOAL>(↑(Submonoid.powers a)).Infinite ↔ ¬IsOfFinOrder a
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : Fin (orderOf x)<GOAL>(finEquivPowers x hx) n = ⟨x ^ ↑n, ⋯⟩
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>hx : IsOfFinAddOrder x<VAR>n : Fin (addOrderOf x)<GOAL>(finEquivMultiples x hx) n = ⟨↑n • x, ⋯⟩
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : ℕ<VAR>hn : ∃ m, x ^ m = x ^ n<GOAL>(finEquivPowers x hx).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, ⋯⟩
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>x : G<VAR>hx : IsOfFinAddOrder x<VAR>n : ℕ<VAR>hn : ∃ m, m • x = n • x<GOAL>(finEquivMultiples x hx).symm ⟨n • x, hn⟩ = ⟨n % addOrderOf x, ⋯⟩
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>a : G<GOAL>Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>a : G<GOAL>Nat.card ↥(Submonoid.powers a) = orderOf a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>IsOfFinAddOrder (-x) ↔ IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>i : ℤ<GOAL>↑(addOrderOf x) ∣ i ↔ i • x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>i : ℤ<GOAL>↑(orderOf x) ∣ i ↔ x ^ i = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>addOrderOf (-x) = addOrderOf x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>orderOf x⁻¹ = orderOf x
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>a : ↥H<GOAL>orderOf ↑a = orderOf a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>a : ↥H<GOAL>addOrderOf ↑a = addOrderOf a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>a : G<VAR>ha : a ∈ H<GOAL>addOrderOf ⟨a, ha⟩ = addOrderOf a
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>a : G<VAR>ha : a ∈ H<GOAL>orderOf ⟨a, ha⟩ = orderOf a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>z : ℤ<GOAL>(z % ↑(addOrderOf x)) • x = z • x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>z : ℤ<GOAL>x ^ (z % ↑(orderOf x)) = x ^ z
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>i : ℤ<GOAL>addOrderOf x • i • x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>i : ℤ<GOAL>(x ^ i) ^ orderOf x = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>h : IsOfFinAddOrder x<VAR>i : ℤ<GOAL>IsOfFinAddOrder (i • x)
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>h : IsOfFinOrder x<VAR>i : ℤ<GOAL>IsOfFinOrder (x ^ i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x y : G<VAR>h : IsOfFinAddOrder x<VAR>h' : y ∈ AddSubgroup.zmultiples x<GOAL>IsOfFinAddOrder y
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<VAR>h : IsOfFinOrder x<VAR>h' : y ∈ Subgroup.zpowers x<GOAL>IsOfFinOrder y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x y : G<VAR>h : y ∈ AddSubgroup.zmultiples x<GOAL>addOrderOf y ∣ addOrderOf x
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<VAR>h : y ∈ Subgroup.zpowers x<GOAL>orderOf y ∣ orderOf x
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<VAR>α : Type u_6<VAR>MulAction G α<VAR>hx : x ∈ Subgroup.zpowers y<VAR>a : α<VAR>hs : y • a = a<GOAL>x • a = a
<VAR>α : Type u_6<VAR>G : Type u_7<VAR>AddGroup G<VAR>AddAction G α<VAR>x y : G<VAR>hx : x ∈ AddSubgroup.zmultiples y<VAR>a : α<VAR>hs : y +ᵥ a = a<GOAL>x +ᵥ a = a
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<VAR>hx : IsOfFinOrder x<GOAL>y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x y : G<VAR>hx : IsOfFinAddOrder x<GOAL>y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>hx : IsOfFinOrder x<GOAL>↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>hx : IsOfFinAddOrder x<GOAL>↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x y : G<VAR>DecidableEq G<VAR>hx : IsOfFinAddOrder x<GOAL>y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<VAR>DecidableEq G<VAR>hx : IsOfFinOrder x<GOAL>y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>hx : IsOfFinAddOrder x<VAR>n : Fin (addOrderOf x)<GOAL>(finEquivZMultiples x hx) n = ⟨↑n • x, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : Fin (orderOf x)<GOAL>(finEquivZPowers x hx) n = ⟨x ^ ↑n, ⋯⟩
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>hx : IsOfFinAddOrder x<VAR>n : ℕ<GOAL>(finEquivZMultiples x hx).symm ⟨n • x, ⋯⟩ = ⟨n % addOrderOf x, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : ℕ<GOAL>(finEquivZPowers x hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>x y : G<VAR>hx : IsOfFinOrder x<VAR>hy : IsOfFinOrder y<GOAL>IsOfFinOrder (x * y)
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>x y : G<VAR>hx : IsOfFinAddOrder x<VAR>hy : IsOfFinAddOrder y<GOAL>IsOfFinAddOrder (x + y)
<VAR>G : Type u_1<VAR>Monoid G<VAR>n : ℕ<VAR>Fintype G<VAR>DecidableEq G<VAR>hn : n ≠ 0<GOAL>∑ m ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ), (Finset.filter (fun x => orderOf x = m) Finset.univ).card = (Finset.filter (fun x => x ^ n = 1) Finset.univ).card
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>n : ℕ<VAR>Fintype G<VAR>DecidableEq G<VAR>hn : n ≠ 0<GOAL>∑ m ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ), (Finset.filter (fun x => addOrderOf x = m) Finset.univ).card = (Finset.filter (fun x => n • x = 0) Finset.univ).card
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>Fintype G<GOAL>addOrderOf x ≤ Fintype.card G
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>Fintype G<GOAL>orderOf x ≤ Fintype.card G
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>x : G<GOAL>IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>x : G<GOAL>IsOfFinOrder x
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>x : G<GOAL>0 < orderOf x
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>x : G<GOAL>0 < addOrderOf x
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>n : ℕ<VAR>x : G<GOAL>orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>n : ℕ<VAR>x : G<GOAL>addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>x y : G<VAR>DecidableEq G<GOAL>y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>x y : G<VAR>DecidableEq G<GOAL>y ∈ Submonoid.powers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>x y : G<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>x y : G<VAR>h : addOrderOf x = addOrderOf y<VAR>n : ℕ<GOAL>(multiplesEquivMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩
<VAR>G : Type u_1<VAR>LeftCancelMonoid G<VAR>Fintype G<VAR>x : G<GOAL>orderOf x = Fintype.card ↑↑(Submonoid.powers x)
<VAR>G : Type u_1<VAR>AddLeftCancelMonoid G<VAR>Fintype G<VAR>x : G<GOAL>addOrderOf x = Fintype.card ↑↑(AddSubmonoid.multiples x)
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<VAR>x : G<GOAL>∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<VAR>x : G<GOAL>∃ i, ∃ (_ : i ≠ 0), i • x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<VAR>x y : G<GOAL>y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<VAR>x y : G<GOAL>y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<VAR>x : G<GOAL>↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<VAR>x : G<GOAL>↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<VAR>x y : G<VAR>DecidableEq G<GOAL>y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<VAR>x y : G<VAR>DecidableEq G<GOAL>y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>n : ℤ<GOAL>x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>n : ℤ<GOAL>n • x = 0 ↔ n ≡ 0 [ZMOD ↑(addOrderOf x)]
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>m n : ℤ<GOAL>m • x = n • x ↔ m ≡ n [ZMOD ↑(addOrderOf x)]
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>m n : ℤ<GOAL>x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>(Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>(Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<VAR>x y : G<VAR>h : addOrderOf x = addOrderOf y<VAR>n : ℕ<GOAL>(zmultiplesEquivZMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<VAR>x y : G<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>x : G<GOAL>Fintype.card ↥(Subgroup.zpowers x) = orderOf x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>x : G<GOAL>Fintype.card ↥(AddSubgroup.zmultiples x) = addOrderOf x
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>a : G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>ha : a ^ k = 1<GOAL>Fintype.card ↥(Subgroup.zpowers a) ≤ k
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>a : G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>ha : k • a = 0<GOAL>Fintype.card ↥(AddSubgroup.zmultiples a) ≤ k
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>x : G<GOAL>orderOf x ∣ Fintype.card G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>x : G<GOAL>addOrderOf x ∣ Fintype.card G
<VAR>G : Type u_6<VAR>AddGroup G<VAR>x : G<GOAL>addOrderOf x ∣ Nat.card G
<VAR>G : Type u_6<VAR>Group G<VAR>x : G<GOAL>orderOf x ∣ Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>s : Subgroup G<VAR>hx : x ∈ s<GOAL>orderOf x ∣ Nat.card ↥s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>s : AddSubgroup G<VAR>hx : x ∈ s<GOAL>addOrderOf x ∣ Nat.card ↥s
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>s : Subgroup G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>orderOf x ≤ Nat.card ↥s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>s : AddSubgroup G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>addOrderOf x ≤ Nat.card ↥s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<VAR>s : AddSubmonoid G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>addOrderOf x ≤ Nat.card ↥s
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>s : Submonoid G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>orderOf x ≤ Nat.card ↥s
<VAR>G : Type u_6<VAR>AddGroup G<VAR>x : G<GOAL>Nat.card G • x = 0
<VAR>G : Type u_6<VAR>Group G<VAR>x : G<GOAL>x ^ Nat.card G = 1
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>x : G<GOAL>x ^ Fintype.card G = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>x : G<GOAL>Fintype.card G • x = 0
<VAR>G : Type u_6<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>H.Normal<VAR>g : G<GOAL>H.index • g ∈ H
<VAR>G : Type u_6<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>g : G<GOAL>g ^ H.index ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>a : G<VAR>n : ℕ<GOAL>(n % Fintype.card G) • a = n • a
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (n % Fintype.card G) = a ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>a : G<VAR>n : ℤ<GOAL>(n % ↑(Fintype.card G)) • a = n • a
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n % ↑(Fintype.card G)) = a ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>n : ℕ<GOAL>(n % Nat.card G) • a = n • a
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (n % Nat.card G) = a ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>(n % ↑(Nat.card G)) • a = n • a
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n % ↑(Nat.card G)) = a ^ n
<VAR>n : ℕ<VAR>G : Type u_6<VAR>AddGroup G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(nsmulCoprime h).symm g = (Nat.card G).gcdB n • g
<VAR>n : ℕ<VAR>G : Type u_6<VAR>AddGroup G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(nsmulCoprime h) g = n • g
<VAR>n : ℕ<VAR>G : Type u_6<VAR>Group G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(powCoprime h).symm g = g ^ (Nat.card G).gcdB n
<VAR>n : ℕ<VAR>G : Type u_6<VAR>Group G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(powCoprime h) g = g ^ n
<VAR>n : ℕ<VAR>G : Type u_6<VAR>Group G<VAR>h : (Nat.card G).Coprime n<GOAL>(powCoprime h) 1 = 1
<VAR>n : ℕ<VAR>G : Type u_6<VAR>AddGroup G<VAR>h : (Nat.card G).Coprime n<GOAL>(nsmulCoprime h) 0 = 0
<VAR>n : ℕ<VAR>G : Type u_6<VAR>Group G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(powCoprime h) g⁻¹ = ((powCoprime h) g)⁻¹
<VAR>n : ℕ<VAR>G : Type u_6<VAR>AddGroup G<VAR>h : (Nat.card G).Coprime n<VAR>g : G<GOAL>(nsmulCoprime h) (-g) = -(nsmulCoprime h) g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>n : ℕ<VAR>hn : (Nat.card G).Coprime n<GOAL>Function.Bijective fun x => n • x
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<VAR>hn : (Nat.card G).Coprime n<GOAL>Function.Bijective fun x => x ^ n
<VAR>G : Type u_6<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : (Nat.card ↥H).Coprime (Nat.card ↥K)<GOAL>H ⊓ K = ⊥
<VAR>G : Type u_6<VAR>Group G<VAR>H K : Subgroup G<VAR>h : (Nat.card ↥H).Coprime (Nat.card ↥K)<GOAL>H ⊓ K = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>x : G<VAR>DecidableEq G<GOAL>Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(Subgroup.zpowers x)).toFinset
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>x : G<VAR>DecidableEq G<GOAL>Finset.image (fun i => i • x) (Finset.range (addOrderOf x)) = (↑(AddSubgroup.zmultiples x)).toFinset
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>x : G<VAR>n : ℕ<GOAL>x ^ n = 1 ↔ x ^ n.gcd (Fintype.card G) = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>x : G<VAR>n : ℕ<GOAL>n • x = 0 ↔ n.gcd (Fintype.card G) • x = 0
<VAR>G : Type u_6<VAR>AddGroup G<VAR>Fintype G<VAR>S : Set G<VAR>hS : S.Nonempty<GOAL>↑(smulCardAddSubgroup S hS) = Fintype.card G • S
<VAR>G : Type u_6<VAR>Group G<VAR>Fintype G<VAR>S : Set G<VAR>hS : S.Nonempty<GOAL>↑(powCardSubgroup S hS) = S ^ Fintype.card G
<VAR>G : Type u_1<VAR>LinearOrderedSemiring G<VAR>a : G<VAR>ha₀ : 0 ≤ a<VAR>ha : IsOfFinOrder a<GOAL>a = 1
<VAR>G : Type u_1<VAR>LinearOrderedRing G<VAR>a : G<VAR>ha₀ : a ≤ 0<VAR>ha : IsOfFinOrder a<GOAL>a = -1
<VAR>G : Type u_1<VAR>LinearOrderedRing G<VAR>x : G<VAR>h : |x| ≠ 1<GOAL>orderOf x = 0
<VAR>G : Type u_1<VAR>LinearOrderedRing G<VAR>x : G<GOAL>orderOf x ≤ 2
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>x : α × β<GOAL>orderOf x = (orderOf x.1).lcm (orderOf x.2)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>x : α × β<GOAL>addOrderOf x = (addOrderOf x.1).lcm (addOrderOf x.2)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>x : α × β<GOAL>addOrderOf x.1 ∣ addOrderOf x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>x : α × β<GOAL>orderOf x.1 ∣ orderOf x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>x : α × β<GOAL>addOrderOf x.2 ∣ addOrderOf x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>x : α × β<GOAL>orderOf x.2 ∣ orderOf x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>x : α × β<VAR>hx : IsOfFinAddOrder x<GOAL>IsOfFinAddOrder x.1
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>x : α × β<VAR>hx : IsOfFinOrder x<GOAL>IsOfFinOrder x.1
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>x : α × β<VAR>hx : IsOfFinAddOrder x<GOAL>IsOfFinAddOrder x.2
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>x : α × β<VAR>hx : IsOfFinOrder x<GOAL>IsOfFinOrder x.2
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>a : α<VAR>b : β<GOAL>IsOfFinAddOrder a → IsOfFinAddOrder b → IsOfFinAddOrder (a, b)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>a : α<VAR>b : β<GOAL>IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>AddMonoid α<VAR>AddMonoid β<VAR>a : α<VAR>b : β<GOAL>addOrderOf (a, b) = (addOrderOf a).lcm (addOrderOf b)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Monoid α<VAR>Monoid β<VAR>a : α<VAR>b : β<GOAL>orderOf (a, b) = (orderOf a).lcm (orderOf b)
<VAR>R : Type u_6<VAR>AddGroupWithOne R<VAR>Fintype R<GOAL>↑(Fintype.card R) = 0
<VAR>R : Type u_6<VAR>NonAssocRing R<GOAL>CharP R (addOrderOf 1)
<VAR>R : Type u_6<VAR>NonAssocRing R<VAR>Fintype R<VAR>p : ℕ<VAR>hn : Fintype.card R = p<VAR>hR : ∀ i < p, ↑i = 0 → i = 0<GOAL>CharP R p
<VAR>R : Type u_6<VAR>Ring R<VAR>Fintype R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : Fintype.card R = p ^ n<VAR>hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n<GOAL>CharP R (p ^ n)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>x y : G<VAR>h : AddSemiconjBy a x y<GOAL>addOrderOf x = addOrderOf y
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>x y : G<VAR>h : SemiconjBy a x y<GOAL>orderOf x = orderOf y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>ι : α ↪ β<VAR>x : α<GOAL>(e.viaEmbedding ι) (ι x) = ι (e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>ι : α ↪ β<VAR>x : β<VAR>hx : x ∉ Set.range ⇑ι<GOAL>(e.viaEmbedding ι) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>ι : α ↪ β<GOAL>(Equiv.Perm.viaEmbeddingHom ι) e = e.viaEmbedding ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : α ↪ β<GOAL>Function.Injective ⇑(Equiv.Perm.viaEmbeddingHom ι)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<GOAL>(CoxeterMatrix.reindex e M).relationsSet = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>i : B'<GOAL>(M.reindexGroupEquiv e) ((CoxeterMatrix.reindex e M).simple i) = M.simple (e.symm i)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>i : B<GOAL>(M.reindexGroupEquiv e).symm (M.simple i) = (CoxeterMatrix.reindex e M).simple (e i)
<VAR>W : Type u<VAR>Group W<VAR>self : IsCoxeterGroup W<GOAL>∃ B M, Nonempty (CoxeterSystem M W)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>e : B ≃ B'<GOAL>(cs.reindex e).mulEquiv = cs.mulEquiv.trans (M.reindexGroupEquiv e).symm
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>H : Type u_4<VAR>Group W<VAR>Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>e : W ≃* H<GOAL>(cs.map e).mulEquiv = e.symm.trans cs.mulEquiv
<VAR>B : Type u_1<VAR>M : CoxeterMatrix B<GOAL>M.toCoxeterSystem.simple = M.simple
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i' : B'<GOAL>(cs.reindex e).simple i' = cs.simple (e.symm i')
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>H : Type u_4<VAR>Group W<VAR>Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>e : W ≃* H<VAR>i : B<GOAL>(cs.map e).simple i = e (cs.simple i)
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.simple i * cs.simple i = 1
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>w * cs.simple i * cs.simple i = w
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.simple i * (cs.simple i * w) = w
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.simple i ^ 2 = 1
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>(cs.simple i)⁻¹ = cs.simple i
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<GOAL>(cs.simple i * cs.simple i') ^ M.M i i' = 1
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<GOAL>(cs.simple i' * cs.simple i) ^ M.M i i' = 1