ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<VAR>σ : Equiv.Perm α<GOAL>Equiv.swap i j * σ = σ ↔ i = j
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<VAR>σ : Equiv.Perm α<GOAL>σ * Equiv.swap i j = σ ↔ i = j
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hxz : x ≠ z<GOAL>Equiv.swap y z * Equiv.swap x y * Equiv.swap y z = Equiv.swap z x
<VAR>α : Type u<VAR>AddGroup α<GOAL>Equiv.addLeft 0 = 1
<VAR>α : Type u<VAR>AddGroup α<GOAL>Equiv.addRight 0 = 1
<VAR>α : Type u<VAR>AddGroup α<VAR>a b : α<GOAL>Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b
<VAR>α : Type u<VAR>AddGroup α<VAR>a b : α<GOAL>Equiv.addRight (a + b) = Equiv.addRight b * Equiv.addRight a
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<GOAL>(Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a)
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<GOAL>(Equiv.addRight a)⁻¹ = Equiv.addRight (-a)
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<VAR>n : ℕ<GOAL>Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<VAR>n : ℕ<GOAL>Equiv.addRight a ^ n = Equiv.addRight (n • a)
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<VAR>n : ℤ<GOAL>Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<VAR>n : ℤ<GOAL>Equiv.addRight a ^ n = Equiv.addRight (n • a)
<VAR>α : Type u<VAR>Group α<GOAL>Equiv.mulLeft 1 = 1
<VAR>α : Type u<VAR>Group α<GOAL>Equiv.mulRight 1 = 1
<VAR>α : Type u<VAR>Group α<VAR>a b : α<GOAL>Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b
<VAR>α : Type u<VAR>Group α<VAR>a b : α<GOAL>Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a
<VAR>α : Type u<VAR>Group α<VAR>a : α<GOAL>(Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>a : α<GOAL>(Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>a : α<VAR>n : ℕ<GOAL>Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
<VAR>α : Type u<VAR>Group α<VAR>a : α<VAR>n : ℕ<GOAL>Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
<VAR>α : Type u<VAR>Group α<VAR>a : α<VAR>n : ℤ<GOAL>Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
<VAR>α : Type u<VAR>Group α<VAR>a : α<VAR>n : ℤ<GOAL>Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hf : Set.BijOn (⇑f) s s<GOAL>Set.BijOn (⇑f⁻¹) s s
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>Set.MapsTo (⇑f) s s → ∀ (n : ℕ), Set.MapsTo (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>Set.SurjOn (⇑f) s s → ∀ (n : ℕ), Set.SurjOn (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>Set.BijOn (⇑f) s s → ∀ (n : ℕ), Set.BijOn (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hf : Set.BijOn (⇑f) s s<VAR>n : ℤ<GOAL>Set.BijOn (⇑(f ^ n)) s s
<VAR>α : Type u<VAR>AddGroup α<VAR>self : IsAddCyclic α<GOAL>∃ g, ∀ (x : α), x ∈ AddSubgroup.zmultiples g
<VAR>α : Type u<VAR>Group α<VAR>self : IsCyclic α<GOAL>∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g
<VAR>α : Type u<VAR>AddGroup α<GOAL>IsCyclic (Multiplicative α) ↔ IsAddCyclic α
<VAR>α : Type u<VAR>Group α<GOAL>IsAddCyclic (Additive α) ↔ IsCyclic α
<VAR>α : Type u<VAR>Group α<VAR>nc : ¬IsCyclic α<GOAL>Nontrivial α
<VAR>α : Type u<VAR>AddGroup α<VAR>nc : ¬IsAddCyclic α<GOAL>Nontrivial α
<VAR>G : Type u_1<VAR>Group G<VAR>h : IsCyclic G<VAR>σ : G →* G<GOAL>∃ m, ∀ (g : G), σ g = g ^ m
<VAR>G : Type u_1<VAR>AddGroup G<VAR>h : IsAddCyclic G<VAR>σ : G →+ G<GOAL>∃ m, ∀ (g : G), σ g = m • g
<VAR>α : Type u<VAR>Group α<VAR>Fintype α<VAR>x : α<VAR>hx : orderOf x = Fintype.card α<GOAL>IsCyclic α
<VAR>α : Type u<VAR>AddGroup α<VAR>Fintype α<VAR>x : α<VAR>hx : addOrderOf x = Fintype.card α<GOAL>IsAddCyclic α
<VAR>G : Type u_1<VAR>Group G<GOAL>∀ {x : Fintype G} (H : Subgroup G) [hp : Fact (Nat.Prime (Fintype.card G))], H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>∀ {x : Fintype G} (H : AddSubgroup G) [hp : Fact (Nat.Prime (Fintype.card G))], H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, g ≠ 0 → AddSubgroup.zmultiples g = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, g ≠ 1 → Subgroup.zpowers g = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Subgroup.zpowers g
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubgroup.zmultiples g
<VAR>G : Type u_1<VAR>Group G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Submonoid.powers g
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubmonoid.multiples g
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, g ≠ 0 → AddSubmonoid.multiples g = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, g ≠ 1 → Submonoid.powers g = ⊤
<VAR>α : Type u<VAR>AddGroup α<VAR>Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<GOAL>IsAddCyclic α
<VAR>α : Type u<VAR>Group α<VAR>Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<GOAL>IsCyclic α
<VAR>α : Type u<VAR>AddGroup α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Nat.card α ∣ p<GOAL>IsAddCyclic α
<VAR>α : Type u<VAR>Group α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Nat.card α ∣ p<GOAL>IsCyclic α
<VAR>H : Type u_1<VAR>G : Type u_2<VAR>F : Type u_3<VAR>Group H<VAR>Group G<VAR>hH : IsCyclic H<VAR>FunLike F H G<VAR>MonoidHomClass F H G<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>IsCyclic G
<VAR>H : Type u_1<VAR>G : Type u_2<VAR>F : Type u_3<VAR>AddGroup H<VAR>AddGroup G<VAR>hH : IsAddCyclic H<VAR>FunLike F H G<VAR>AddMonoidHomClass F H G<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>IsAddCyclic G
<VAR>α : Type u<VAR>AddGroup α<VAR>Fintype α<VAR>g : α<VAR>hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g<GOAL>addOrderOf g = Fintype.card α
<VAR>α : Type u<VAR>Group α<VAR>Fintype α<VAR>g : α<VAR>hx : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>orderOf g = Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>Group α<VAR>h : ∀ (x : α), x ∈ Subgroup.zpowers a<GOAL>orderOf a = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>AddGroup α<VAR>h : ∀ (x : α), x ∈ AddSubgroup.zmultiples a<GOAL>addOrderOf a = Nat.card α
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>G_cyclic : IsAddCyclic G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card G<GOAL>∃ a, k • a ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>G_cyclic : IsCyclic G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card G<GOAL>∃ a, a ^ k ≠ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>Infinite α<VAR>g : α<VAR>h : ∀ (x : α), x ∈ AddSubgroup.zmultiples g<GOAL>addOrderOf g = 0
<VAR>α : Type u<VAR>Group α<VAR>Infinite α<VAR>g : α<VAR>h : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>orderOf g = 0
<VAR>α : Type u<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>IsAddCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<GOAL>(Finset.filter (fun a => n • a = 0) Finset.univ).card ≤ n
<VAR>α : Type u<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<GOAL>(Finset.filter (fun a => a ^ n = 1) Finset.univ).card ≤ n
<VAR>α : Type u<VAR>Group α<VAR>Finite α<VAR>IsCyclic α<GOAL>∃ x, ∀ (y : α), y ∈ Submonoid.powers x
<VAR>α : Type u<VAR>AddGroup α<VAR>Finite α<VAR>IsAddCyclic α<GOAL>∃ x, ∀ (y : α), y ∈ AddSubmonoid.multiples x
<VAR>α : Type u<VAR>Group α<VAR>h : IsCyclic α<GOAL>∃ g, orderOf g = Nat.card α
<VAR>α : Type u<VAR>AddGroup α<VAR>h : IsAddCyclic α<GOAL>∃ g, addOrderOf g = Nat.card α
<VAR>α : Type u<VAR>Group α<VAR>Finite α<GOAL>IsCyclic α ↔ ∃ g, orderOf g = Nat.card α
<VAR>α : Type u<VAR>AddGroup α<VAR>Finite α<GOAL>IsAddCyclic α ↔ ∃ g, addOrderOf g = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ Subgroup.zpowers a<GOAL>Finset.image (fun i => a ^ i) (Finset.range (orderOf a)) = Finset.univ
<VAR>α : Type u<VAR>a : α<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a<GOAL>Finset.image (fun i => i • a) (Finset.range (addOrderOf a)) = Finset.univ
<VAR>α : Type u<VAR>a : α<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a<GOAL>Finset.image (fun i => i • a) (Finset.range (Fintype.card α)) = Finset.univ
<VAR>α : Type u<VAR>a : α<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ Subgroup.zpowers a<GOAL>Finset.image (fun i => a ^ i) (Finset.range (Fintype.card α)) = Finset.univ
<VAR>α : Type u<VAR>a : α<VAR>Group α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ Subgroup.zpowers a<VAR>x : α<GOAL>∃! n, x = a ^ n.val
<VAR>α : Type u<VAR>a : α<VAR>AddGroup α<VAR>Fintype α<VAR>ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a<VAR>x : α<GOAL>∃! n, x = n.val • a
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>IsCyclic G<VAR>d : ℕ<VAR>a b : ZMod d<VAR>hGcard : Fintype.card G = d<VAR>h : ∀ (t : G), t ^ a.val = t ^ b.val<GOAL>a = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>IsAddCyclic G<VAR>d : ℕ<VAR>a b : ZMod d<VAR>hGcard : Fintype.card G = d<VAR>h : ∀ (t : G), a.val • t = b.val • t<GOAL>a = b
<VAR>α : Type u<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => a ^ n = 1) Finset.univ).card ≤ n<VAR>a : α<GOAL>(Finset.filter (fun b => b ^ orderOf a = 1) Finset.univ).card = orderOf a
<VAR>α : Type u<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => n • a = 0) Finset.univ).card ≤ n<VAR>a : α<GOAL>(Finset.filter (fun b => addOrderOf a • b = 0) Finset.univ).card = addOrderOf a
<VAR>α : Type u<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => a ^ n = 1) Finset.univ).card ≤ n<VAR>d : ℕ<GOAL>d ∣ Fintype.card α → 0 < (Finset.filter (fun a => orderOf a = d) Finset.univ).card → (Finset.filter (fun a => orderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => n • a = 0) Finset.univ).card ≤ n<VAR>d : ℕ<GOAL>d ∣ Fintype.card α → 0 < (Finset.filter (fun a => addOrderOf a = d) Finset.univ).card → (Finset.filter (fun a => addOrderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => a ^ n = 1) Finset.univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<GOAL>(Finset.filter (fun a => orderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => n • a = 0) Finset.univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<GOAL>(Finset.filter (fun a => addOrderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>AddGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => n • a = 0) Finset.univ).card ≤ n<GOAL>IsAddCyclic α
<VAR>α : Type u<VAR>Group α<VAR>DecidableEq α<VAR>Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun a => a ^ n = 1) Finset.univ).card ≤ n<GOAL>IsCyclic α
<VAR>α : Type u<VAR>Group α<VAR>IsCyclic α<VAR>Fintype α<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<GOAL>(Finset.filter (fun a => orderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>AddGroup α<VAR>IsAddCyclic α<VAR>Fintype α<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<GOAL>(Finset.filter (fun a => addOrderOf a = d) Finset.univ).card = d.totient
<VAR>α : Type u<VAR>Group α<VAR>Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<GOAL>IsSimpleGroup α
<VAR>α : Type u<VAR>AddGroup α<VAR>Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<GOAL>IsSimpleAddGroup α
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>IsCyclic H<VAR>f : G →* H<VAR>hf : f.ker ≤ Subgroup.center G<VAR>a b : G<GOAL>a * b = b * a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>IsAddCyclic H<VAR>f : G →+ H<VAR>hf : f.ker ≤ AddSubgroup.center G<VAR>a b : G<GOAL>a + b = b + a
<VAR>α : Type u<VAR>CommGroup α<VAR>IsSimpleGroup α<VAR>Fintype α<GOAL>Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>AddCommGroup α<VAR>IsSimpleAddGroup α<VAR>Fintype α<GOAL>Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>Fintype α<VAR>CommGroup α<GOAL>IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>Fintype α<VAR>AddCommGroup α<GOAL>IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>AddGroup α<VAR>IsAddCyclic α<VAR>Fintype α<GOAL>AddMonoid.exponent α = Fintype.card α
<VAR>α : Type u<VAR>Group α<VAR>IsCyclic α<VAR>Fintype α<GOAL>Monoid.exponent α = Fintype.card α
<VAR>α : Type u<VAR>AddCommGroup α<VAR>Fintype α<VAR>h : AddMonoid.exponent α = Fintype.card α<GOAL>IsAddCyclic α
<VAR>α : Type u<VAR>CommGroup α<VAR>Fintype α<VAR>h : Monoid.exponent α = Fintype.card α<GOAL>IsCyclic α
<VAR>α : Type u<VAR>CommGroup α<VAR>Fintype α<GOAL>IsCyclic α ↔ Monoid.exponent α = Fintype.card α
<VAR>α : Type u<VAR>AddCommGroup α<VAR>Fintype α<GOAL>IsAddCyclic α ↔ AddMonoid.exponent α = Fintype.card α
<VAR>α : Type u<VAR>Group α<VAR>IsCyclic α<VAR>Infinite α<GOAL>Monoid.exponent α = 0
<VAR>α : Type u<VAR>AddGroup α<VAR>IsAddCyclic α<VAR>Infinite α<GOAL>AddMonoid.exponent α = 0
<VAR>n : ℕ<GOAL>AddMonoid.exponent (ZMod n) = n
<VAR>α : Type u<VAR>AddGroup α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<GOAL>¬IsAddCyclic α ↔ AddMonoid.exponent α = p
<VAR>α : Type u<VAR>Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<GOAL>¬IsCyclic α ↔ Monoid.exponent α = p
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>((zmultiplesHom G) g).ker = AddSubgroup.zmultiples ↑(addOrderOf g)
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>((zpowersHom G) g).ker = Subgroup.zpowers (Multiplicative.ofAdd ↑(orderOf g))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>g' : G'<VAR>hg' : addOrderOf g' ∣ addOrderOf g<GOAL>(addMonoidHomOfForallMemZmultiples hg hg') g = g'
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>(monoidHomOfForallMemZpowers hg hg') g = g'
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>f₁ f₂ : G →+ G'<GOAL>f₁ = f₂ ↔ f₁ g = f₂ g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>f₁ f₂ : G →* G'<GOAL>f₁ = f₂ ↔ f₁ g = f₂ g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>f₁ f₂ : G ≃* G'<GOAL>f₁ = f₂ ↔ f₁ g = f₂ g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>f₁ f₂ : G ≃+ G'<GOAL>f₁ = f₂ ↔ f₁ g = f₂ g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g'<VAR>h : addOrderOf g = addOrderOf g'<GOAL>(addEquivOfAddOrderOfEq hg hg' h) g = g'
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g'<VAR>h : orderOf g = orderOf g'<GOAL>(mulEquivOfOrderOfEq hg hg' h) g = g'
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g'<VAR>h : orderOf g = orderOf g'<GOAL>(mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g'<VAR>h : addOrderOf g = addOrderOf g'<GOAL>(addEquivOfAddOrderOfEq hg hg' h).symm = addEquivOfAddOrderOfEq hg' hg ⋯
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g'<VAR>h : addOrderOf g = addOrderOf g'<GOAL>(addEquivOfAddOrderOfEq hg hg' h).symm g' = g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ Subgroup.zpowers g<VAR>g' : G'<VAR>hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g'<VAR>h : orderOf g = orderOf g'<GOAL>(mulEquivOfOrderOfEq hg hg' h).symm g' = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H.IsComplement' K ↔ AddSubgroup.IsComplement ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H.IsComplement' K ↔ Subgroup.IsComplement ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<GOAL>Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<GOAL>AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 + ↑x.2 = g
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>h : Subgroup.IsComplement S T<VAR>g : G<GOAL>∃! x, ↑x.1 * ↑x.2 = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<VAR>h : AddSubgroup.IsComplement S T<VAR>g : G<GOAL>∃! x, ↑x.1 + ↑x.2 = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H.IsComplement' K<GOAL>K.IsComplement' H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>K.IsComplement' H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H.IsComplement' K ↔ K.IsComplement' H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H.IsComplement' K ↔ K.IsComplement' H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>AddSubgroup.IsComplement Set.univ {g}
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>Subgroup.IsComplement Set.univ {g}
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>Subgroup.IsComplement {g} Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>AddSubgroup.IsComplement {g} Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>g : G<GOAL>Subgroup.IsComplement {g} S ↔ S = Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<VAR>g : G<GOAL>AddSubgroup.IsComplement {g} S ↔ S = Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<VAR>g : G<GOAL>AddSubgroup.IsComplement S {g} ↔ S = Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>g : G<GOAL>Subgroup.IsComplement S {g} ↔ S = Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<GOAL>AddSubgroup.IsComplement Set.univ S ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<GOAL>Subgroup.IsComplement Set.univ S ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<GOAL>AddSubgroup.IsComplement S Set.univ ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<GOAL>Subgroup.IsComplement S Set.univ ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>h : Subgroup.IsComplement S T<GOAL>S * T = Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<VAR>h : AddSubgroup.IsComplement S T<GOAL>S + T = Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>h : Subgroup.IsComplement S T<GOAL>Nat.card ↑S * Nat.card ↑T = Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<VAR>h : AddSubgroup.IsComplement S T<GOAL>Nat.card ↑S * Nat.card ↑T = Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊤.IsComplement' ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>⊤.IsComplement' ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>⊥.IsComplement' ⊤
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊥.IsComplement' ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊥.IsComplement' H ↔ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊥.IsComplement' H ↔ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.IsComplement' ⊥ ↔ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.IsComplement' ⊥ ↔ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊤.IsComplement' H ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊤.IsComplement' H ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.IsComplement' ⊤ ↔ H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.IsComplement' ⊤ ↔ H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<GOAL>S ∈ Subgroup.leftTransversals T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<GOAL>S ∈ AddSubgroup.leftTransversals T ↔ ∀ (g : G), ∃! s, -↑s + g ∈ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : Set G<GOAL>S ∈ AddSubgroup.rightTransversals T ↔ ∀ (g : G), ∃! s, g + -↑s ∈ T
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<GOAL>S ∈ Subgroup.rightTransversals T ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<GOAL>S ∈ Subgroup.leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<GOAL>S ∈ AddSubgroup.leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientAddGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<GOAL>S ∈ Subgroup.rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<GOAL>S ∈ AddSubgroup.rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientAddGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<GOAL>S ∈ Subgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<GOAL>S ∈ AddSubgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<GOAL>S ∈ AddSubgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<GOAL>S ∈ Subgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>h : S ∈ Subgroup.leftTransversals ↑H<GOAL>Nat.card ↑S = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>h : S ∈ AddSubgroup.leftTransversals ↑H<GOAL>Nat.card ↑S = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>h : S ∈ AddSubgroup.rightTransversals ↑H<GOAL>Nat.card ↑S = H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>h : S ∈ Subgroup.rightTransversals ↑H<GOAL>Nat.card ↑S = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<GOAL>Set.range f ∈ AddSubgroup.leftTransversals ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<GOAL>Set.range f ∈ Subgroup.leftTransversals ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>f : Quotient (QuotientGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q<GOAL>Set.range f ∈ Subgroup.rightTransversals ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>f : Quotient (QuotientAddGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q<GOAL>Set.range f ∈ AddSubgroup.rightTransversals ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>∃ S ∈ Subgroup.leftTransversals ↑H, g ∈ S
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<GOAL>∃ S ∈ AddSubgroup.leftTransversals ↑H, g ∈ S
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<GOAL>∃ S ∈ AddSubgroup.rightTransversals ↑H, g ∈ S
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>∃ S ∈ Subgroup.rightTransversals ↑H, g ∈ S
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H' H : AddSubgroup G<VAR>h : H' ≤ H<GOAL>∃ S, S + ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
<VAR>G : Type u_1<VAR>Group G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<GOAL>∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
<VAR>G : Type u_1<VAR>Group G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<GOAL>∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H