ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>Monoid G<VAR>h : Monoid.ExponentExists G<VAR>g : G<GOAL>0 < orderOf g
<VAR>G : Type u<VAR>AddMonoid G<VAR>h : AddMonoid.ExponentExists G<VAR>g : G<GOAL>0 < addOrderOf g
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent G ≠ 0 ↔ Monoid.ExponentExists G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent G ≠ 0 ↔ AddMonoid.ExponentExists G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.ExponentExists G ↔ AddMonoid.exponent G ≠ 0
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.ExponentExists G ↔ Monoid.exponent G ≠ 0
<VAR>G : Type u<VAR>Monoid G<GOAL>0 < Monoid.exponent G ↔ Monoid.ExponentExists G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>0 < AddMonoid.exponent G ↔ AddMonoid.ExponentExists G
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent G = 0 ↔ ¬Monoid.ExponentExists G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent G = 0 ↔ ¬AddMonoid.ExponentExists G
<VAR>G : Type u<VAR>Monoid G<VAR>g : G<VAR>hg : orderOf g = 0<GOAL>Monoid.exponent G = 0
<VAR>G : Type u<VAR>AddMonoid G<VAR>g : G<VAR>hg : addOrderOf g = 0<GOAL>AddMonoid.exponent G = 0
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent G = 0 ↔ ∀ n > 0, ∃ g, n • g ≠ 0
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
<VAR>G : Type u<VAR>Monoid G<VAR>g : G<GOAL>g ^ Monoid.exponent G = 1
<VAR>G : Type u<VAR>AddMonoid G<VAR>g : G<GOAL>AddMonoid.exponent G • g = 0
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<VAR>g : G<GOAL>n • g = (n % AddMonoid.exponent G) • g
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<VAR>g : G<GOAL>g ^ n = g ^ (n % Monoid.exponent G)
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>0 < Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), n • g = 0<GOAL>0 < AddMonoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), n • g = 0<GOAL>AddMonoid.exponent G ≤ n
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>Monoid.exponent G ≤ n
<VAR>G : Type u<VAR>AddMonoid G<VAR>m : ℕ<VAR>hpos : 0 < m<VAR>hm : m < AddMonoid.exponent G<GOAL>∃ g, m • g ≠ 0
<VAR>G : Type u<VAR>Monoid G<VAR>m : ℕ<VAR>hpos : 0 < m<VAR>hm : m < Monoid.exponent G<GOAL>∃ g, g ^ m ≠ 1
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent G = 1 ↔ Subsingleton G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent G = 1 ↔ Subsingleton G
<VAR>G : Type u<VAR>AddMonoid G<VAR>hs : Subsingleton G<GOAL>AddMonoid.exponent G = 1
<VAR>G : Type u<VAR>Monoid G<VAR>hs : Subsingleton G<GOAL>Monoid.exponent G = 1
<VAR>G : Type u<VAR>Monoid G<VAR>g : G<GOAL>orderOf g ∣ Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>g : G<GOAL>addOrderOf g ∣ AddMonoid.exponent G
<VAR>G : Type u<VAR>Monoid G<VAR>h : Monoid.ExponentExists G<VAR>g : G<GOAL>orderOf g ≤ Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>h : AddMonoid.ExponentExists G<VAR>g : G<GOAL>addOrderOf g ≤ AddMonoid.exponent G
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>Monoid.exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<GOAL>AddMonoid.exponent G ∣ n ↔ ∀ (g : G), n • g = 0
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>Monoid.exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<GOAL>AddMonoid.exponent G ∣ n ↔ ∀ (g : G), addOrderOf g ∣ n
<VAR>G : Type u<VAR>AddMonoid G<VAR>n : ℕ<VAR>h : ∀ (g : G), addOrderOf g ∣ n<GOAL>AddMonoid.exponent G ∣ n
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<VAR>h : ∀ (g : G), orderOf g ∣ n<GOAL>Monoid.exponent G ∣ n
<VAR>G : Type u<VAR>AddMonoid G<VAR>Fintype G<GOAL>Finset.univ.lcm addOrderOf ∣ AddMonoid.exponent G
<VAR>G : Type u<VAR>Monoid G<VAR>Fintype G<GOAL>Finset.univ.lcm orderOf ∣ Monoid.exponent G
<VAR>G : Type u<VAR>Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>∃ g, orderOf g = p ^ (Monoid.exponent G).factorization p
<VAR>G : Type u<VAR>AddMonoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>∃ g, addOrderOf g = p ^ (AddMonoid.exponent G).factorization p
<VAR>G : Type u<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) * y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)
<VAR>G : Type u<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<VAR>hx : addOrderOf x ≠ 0<VAR>hy : addOrderOf y ≠ 0<GOAL>addOrderOf ((addOrderOf x / (addOrderOf x).factorizationLCMLeft (addOrderOf y)) • x + (addOrderOf y / (addOrderOf x).factorizationLCMRight (addOrderOf y)) • y) = (addOrderOf x).lcm (addOrderOf y)
<VAR>G : Type u<VAR>Monoid G<VAR>x y : G<VAR>h : Commute x y<GOAL>∃ z ∈ Submonoid.closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
<VAR>G : Type u<VAR>AddMonoid G<VAR>x y : G<VAR>h : AddCommute x y<GOAL>∃ z ∈ AddSubmonoid.closure {x, y}, addOrderOf z = (addOrderOf x).lcm (addOrderOf y)
<VAR>G : Type u_1<VAR>Monoid G<VAR>Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>Monoid.exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>AddMonoid.exponent G = p ↔ ∀ (g : G), g ≠ 0 → addOrderOf g = p
<VAR>G : Type u<VAR>Monoid G<VAR>h : ∀ (g : G), 0 < orderOf g<GOAL>Monoid.exponent G ≠ 0 ↔ (Set.range orderOf).Finite
<VAR>G : Type u<VAR>AddMonoid G<VAR>h : ∀ (g : G), 0 < addOrderOf g<GOAL>AddMonoid.exponent G ≠ 0 ↔ (Set.range addOrderOf).Finite
<VAR>G : Type u<VAR>AddMonoid G<VAR>h : ∀ (g : G), 0 < addOrderOf g<GOAL>AddMonoid.exponent G = 0 ↔ (Set.range addOrderOf).Infinite
<VAR>G : Type u<VAR>Monoid G<VAR>h : ∀ (g : G), 0 < orderOf g<GOAL>Monoid.exponent G = 0 ↔ (Set.range orderOf).Infinite
<VAR>G : Type u<VAR>Monoid G<VAR>Fintype G<GOAL>Finset.univ.lcm orderOf = Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>Fintype G<GOAL>Finset.univ.lcm addOrderOf = AddMonoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>H : Type u_1<VAR>AddMonoid H<VAR>e : G →+ H<VAR>e_inj : Function.Injective ⇑e<GOAL>AddMonoid.exponent G ∣ AddMonoid.exponent H
<VAR>G : Type u<VAR>Monoid G<VAR>H : Type u_1<VAR>Monoid H<VAR>e : G →* H<VAR>e_inj : Function.Injective ⇑e<GOAL>Monoid.exponent G ∣ Monoid.exponent H
<VAR>G : Type u<VAR>Monoid G<VAR>H : Type u_1<VAR>Monoid H<VAR>e : G ≃* H<GOAL>Monoid.exponent G = Monoid.exponent H
<VAR>G : Type u<VAR>AddMonoid G<VAR>H : Type u_1<VAR>AddMonoid H<VAR>e : G ≃+ H<GOAL>AddMonoid.exponent G = AddMonoid.exponent H
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent ↥⊤ = Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent ↥⊤ = AddMonoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>S : AddSubmonoid G<VAR>g : G<VAR>g_in_s : g ∈ S<GOAL>AddMonoid.exponent ↥S • g = 0
<VAR>G : Type u<VAR>Monoid G<VAR>S : Submonoid G<VAR>g : G<VAR>g_in_s : g ∈ S<GOAL>g ^ Monoid.exponent ↥S = 1
<VAR>G : Type u<VAR>AddLeftCancelMonoid G<VAR>Finite G<GOAL>AddMonoid.ExponentExists G
<VAR>G : Type u<VAR>LeftCancelMonoid G<VAR>Finite G<GOAL>Monoid.ExponentExists G
<VAR>G : Type u<VAR>AddLeftCancelMonoid G<VAR>Finite G<GOAL>AddMonoid.exponent G ≠ 0
<VAR>G : Type u<VAR>LeftCancelMonoid G<VAR>Finite G<GOAL>Monoid.exponent G ≠ 0
<VAR>G : Type u<VAR>LeftCancelMonoid G<VAR>Finite G<VAR>Nontrivial G<GOAL>1 < Monoid.exponent G
<VAR>G : Type u<VAR>AddLeftCancelMonoid G<VAR>Finite G<VAR>Nontrivial G<GOAL>1 < AddMonoid.exponent G
<VAR>G : Type u<VAR>CommMonoid G<VAR>hG : Monoid.ExponentExists G<GOAL>∃ g, orderOf g = Monoid.exponent G
<VAR>G : Type u<VAR>AddCommMonoid G<VAR>hG : AddMonoid.ExponentExists G<GOAL>∃ g, addOrderOf g = AddMonoid.exponent G
<VAR>G : Type u<VAR>CommMonoid G<VAR>h : ∀ (g : G), 0 < orderOf g<GOAL>Monoid.exponent G = ⨆ g, orderOf g
<VAR>G : Type u<VAR>AddCommMonoid G<VAR>h : ∀ (g : G), 0 < addOrderOf g<GOAL>AddMonoid.exponent G = ⨆ g, addOrderOf g
<VAR>G : Type u<VAR>CommMonoid G<GOAL>Monoid.exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g
<VAR>G : Type u<VAR>AddCommMonoid G<GOAL>AddMonoid.exponent G = if ∃ g, addOrderOf g = 0 then 0 else ⨆ g, addOrderOf g
<VAR>G : Type u<VAR>CancelCommMonoid G<VAR>Fintype G<GOAL>Monoid.exponent G = (Finset.image orderOf Finset.univ).max' ⋯
<VAR>G : Type u<VAR>AddCancelCommMonoid G<VAR>Fintype G<GOAL>AddMonoid.exponent G = (Finset.image addOrderOf Finset.univ).max' ⋯
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>Nontrivial G<GOAL>1 < Monoid.exponent G
<VAR>G : Type u<VAR>AddGroup G<VAR>Finite G<VAR>Nontrivial G<GOAL>1 < AddMonoid.exponent G
<VAR>G : Type u<VAR>Group G<VAR>Fintype G<GOAL>Monoid.exponent G ∣ Fintype.card G
<VAR>G : Type u<VAR>Group G<GOAL>Monoid.exponent G ∣ Nat.card G
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<GOAL>Monoid.exponent ↥H.toSubmonoid = Monoid.exponent ↥H
<VAR>G : Type u<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>AddMonoid.exponent ↥H.toAddSubmonoid = AddMonoid.exponent ↥H
<VAR>G : Type u<VAR>Group G<GOAL>Monoid.exponent ↥⊤ = Monoid.exponent G
<VAR>G : Type u<VAR>AddGroup G<GOAL>AddMonoid.exponent ↥⊤ = AddMonoid.exponent G
<VAR>G : Type u<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<VAR>g_in_H : g ∈ H<GOAL>AddMonoid.exponent ↥H • g = 0
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>g_in_H : g ∈ H<GOAL>g ^ Monoid.exponent ↥H = 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → AddMonoid (M i)<VAR>j : ι<VAR>hj : AddMonoid.exponent (M j) = 0<GOAL>AddMonoid.exponent ((i : ι) → M i) = 0
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<VAR>j : ι<VAR>hj : Monoid.exponent (M j) = 0<GOAL>Monoid.exponent ((i : ι) → M i) = 0
<VAR>F : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>AddMonoid M₁<VAR>AddMonoid M₂<VAR>FunLike F M₁ M₂<VAR>AddMonoidHomClass F M₁ M₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>AddMonoid.exponent M₂ ∣ AddMonoid.exponent M₁
<VAR>F : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>Monoid M₁<VAR>Monoid M₂<VAR>FunLike F M₁ M₂<VAR>MonoidHomClass F M₁ M₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Monoid.exponent M₂ ∣ Monoid.exponent M₁
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : ι → Type u_2<VAR>(i : ι) → AddMonoid (M i)<GOAL>AddMonoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => AddMonoid.exponent (M x)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : ι → Type u_2<VAR>(i : ι) → Monoid (M i)<GOAL>Monoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => Monoid.exponent (M x)
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>Monoid M₁<VAR>Monoid M₂<GOAL>Monoid.exponent (M₁ × M₂) = lcm (Monoid.exponent M₁) (Monoid.exponent M₂)
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>AddMonoid M₁<VAR>AddMonoid M₂<GOAL>AddMonoid.exponent (M₁ × M₂) = lcm (AddMonoid.exponent M₁) (AddMonoid.exponent M₂)
<VAR>G : Type u<VAR>Monoid G<VAR>hG : Monoid.exponent G = 2<VAR>x : G<GOAL>orderOf x = 2 ↔ x ≠ 1
<VAR>G : Type u<VAR>AddMonoid G<VAR>hG : AddMonoid.exponent G = 2<VAR>x : G<GOAL>addOrderOf x = 2 ↔ x ≠ 0
<VAR>G : Type u<VAR>Monoid G<VAR>IsCancelMul G<VAR>h : ∀ (g : G), orderOf g ∣ 2<VAR>a b : G<GOAL>Commute a b
<VAR>G : Type u<VAR>AddMonoid G<VAR>IsCancelAdd G<VAR>h : ∀ (g : G), addOrderOf g ∣ 2<VAR>a b : G<GOAL>AddCommute a b
<VAR>G : Type u<VAR>Monoid G<VAR>IsCancelMul G<VAR>hG : Monoid.exponent G = 2<VAR>a b : G<GOAL>a * b = b * a
<VAR>G : Type u<VAR>AddMonoid G<VAR>IsCancelAdd G<VAR>hG : AddMonoid.exponent G = 2<VAR>a b : G<GOAL>a + b = b + a
<VAR>G : Type u<VAR>Group G<VAR>hG : Monoid.exponent G = 2<VAR>x : G<GOAL>x⁻¹ = x
<VAR>G : Type u<VAR>AddGroup G<VAR>hG : AddMonoid.exponent G = 2<VAR>x : G<GOAL>-x = x
<VAR>G : Type u<VAR>AddGroup G<VAR>x : G<VAR>hx : addOrderOf x = 2<GOAL>-x = x
<VAR>G : Type u<VAR>Group G<VAR>x : G<VAR>hx : orderOf x = 2<GOAL>x⁻¹ = x
<VAR>G : Type u<VAR>AddGroup G<VAR>x y : G<VAR>hx : addOrderOf x = 2<VAR>hy : addOrderOf y = 2<VAR>hxy : x ≠ y<GOAL>x + y ∉ {x, y, 0}
<VAR>G : Type u<VAR>Group G<VAR>x y : G<VAR>hx : orderOf x = 2<VAR>hy : orderOf y = 2<VAR>hxy : x ≠ y<GOAL>x * y ∉ {x, y, 1}
<VAR>G : Type u<VAR>AddGroup G<VAR>h : AddMonoid.exponent G = 2<VAR>x y : G<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x ≠ y<GOAL>x + y ∉ {x, y, 0}
<VAR>G : Type u<VAR>Group G<VAR>h : Monoid.exponent G = 2<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>x * y ∉ {x, y, 1}
<VAR>S : Type u_1<VAR>R : outParam (Type u_2)<VAR>M : Type u_3<VAR>SMul R M<VAR>SetLike S M<VAR>self : SMulMemClass S R M<VAR>s : S<VAR>r : R<VAR>m : M<GOAL>m ∈ s → r • m ∈ s
<VAR>S : Type u_1<VAR>R : outParam (Type u_2)<VAR>M : Type u_3<VAR>VAdd R M<VAR>SetLike S M<VAR>self : VAddMemClass S R M<VAR>s : S<VAR>r : R<VAR>m : M<GOAL>m ∈ s → r +ᵥ m ∈ s
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>AddMonoid M<VAR>SetLike S M<VAR>AddSubmonoidClass S M<GOAL>SMulMemClass S ℕ M
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>SubNegMonoid M<VAR>SetLike S M<VAR>AddSubgroupClass S M<GOAL>SMulMemClass S ℤ M
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Type u_4<VAR>SetLike S α<VAR>SMul M N<VAR>SMul M α<VAR>Monoid N<VAR>MulAction N α<VAR>SMulMemClass S N α<VAR>IsScalarTower M N α<GOAL>SMulMemClass S M α
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>SetLike S M<VAR>hS : SMulMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : ↥s<GOAL>↑(r • x) = r • ↑x
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>VAdd R M<VAR>SetLike S M<VAR>hS : VAddMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : ↥s<GOAL>↑(r +ᵥ x) = r +ᵥ ↑x
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>VAdd R M<VAR>SetLike S M<VAR>hS : VAddMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : M<VAR>hx : x ∈ s<GOAL>r +ᵥ ⟨x, hx⟩ = ⟨r +ᵥ x, ⋯⟩
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>SetLike S M<VAR>hS : SMulMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : M<VAR>hx : x ∈ s<GOAL>r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>VAdd R M<VAR>SetLike S M<VAR>hS : VAddMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : ↥s<GOAL>r +ᵥ x = ⟨r +ᵥ ↑x, ⋯⟩
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>SetLike S M<VAR>hS : SMulMemClass S R M<VAR>s : S<VAR>r : R<VAR>x : ↥s<GOAL>r • x = ⟨r • ↑x, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>Monoid R<VAR>MulAction R M<VAR>SetLike S M<VAR>SMulMemClass S R M<VAR>N : S<VAR>x : M<GOAL>(∀ (a : R), a • x ∈ N) ↔ x ∈ N
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>SMul M N<VAR>SMul M α<VAR>Monoid N<VAR>MulAction N α<VAR>SMulMemClass S N α<VAR>IsScalarTower M N α<VAR>s : S<VAR>r : M<VAR>x : ↥s<GOAL>↑(r • x) = r • ↑x
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>VAdd M N<VAR>VAdd M α<VAR>AddMonoid N<VAR>AddAction N α<VAR>VAddMemClass S N α<VAR>VAddAssocClass M N α<VAR>s : S<VAR>r : M<VAR>x : ↥s<GOAL>↑(r +ᵥ x) = r +ᵥ ↑x
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>SMul M N<VAR>SMul M α<VAR>Monoid N<VAR>MulAction N α<VAR>SMulMemClass S N α<VAR>IsScalarTower M N α<VAR>s : S<VAR>r : M<VAR>x : α<VAR>hx : x ∈ s<GOAL>r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>VAdd M N<VAR>VAdd M α<VAR>AddMonoid N<VAR>AddAction N α<VAR>VAddMemClass S N α<VAR>VAddAssocClass M N α<VAR>s : S<VAR>r : M<VAR>x : α<VAR>hx : x ∈ s<GOAL>r +ᵥ ⟨x, hx⟩ = ⟨r +ᵥ x, ⋯⟩
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>SMul M N<VAR>SMul M α<VAR>Monoid N<VAR>MulAction N α<VAR>SMulMemClass S N α<VAR>IsScalarTower M N α<VAR>s : S<VAR>r : M<VAR>x : ↥s<GOAL>r • x = ⟨r • ↑x, ⋯⟩
<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type u_1<VAR>α : Type u_2<VAR>SetLike S α<VAR>VAdd M N<VAR>VAdd M α<VAR>AddMonoid N<VAR>AddAction N α<VAR>VAddMemClass S N α<VAR>VAddAssocClass M N α<VAR>s : S<VAR>r : M<VAR>x : ↥s<GOAL>r +ᵥ x = ⟨r +ᵥ ↑x, ⋯⟩
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>self : SubMulAction R M<VAR>c : R<VAR>x : M<GOAL>x ∈ self.carrier → c • x ∈ self.carrier
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>x : M<GOAL>x ∈ p.carrier ↔ x ∈ ↑p
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p q : SubMulAction R M<VAR>h : ∀ (x : M), x ∈ p ↔ x ∈ q<GOAL>p = q
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>s : Set M<VAR>hs : s = ↑p<GOAL>↑(p.copy s hs) = s
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>s : Set M<VAR>hs : s = ↑p<GOAL>p.copy s hs = p
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>x : M<VAR>r : R<VAR>h : x ∈ p<GOAL>r • x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>r : R<VAR>x : ↥p<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<VAR>x : ↥p<GOAL>p.subtype x = ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>p : SubMulAction R M<GOAL>⇑p.subtype = Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>A : Type u_1<VAR>SetLike A M<VAR>hA : SMulMemClass A R M<VAR>S' : A<GOAL>⇑(SubMulAction.SMulMemClass.subtype S') = Subtype.val
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>SMul S R<VAR>SMul S M<VAR>IsScalarTower S R M<VAR>p : SubMulAction R M<VAR>s : S<VAR>x : M<VAR>h : x ∈ p<GOAL>s • x ∈ p
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>SMul S R<VAR>SMul S M<VAR>IsScalarTower S R M<VAR>p : SubMulAction R M<VAR>s : S<VAR>x : ↥p<GOAL>↑(s • x) = s • ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>G : Type u_1<VAR>Group G<VAR>SMul G R<VAR>MulAction G M<VAR>IsScalarTower G R M<VAR>g : G<VAR>x : M<GOAL>g • x ∈ p ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>Subtype.val '' MulAction.orbit R m = MulAction.orbit R ↑m
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>x m : ↥p<GOAL>x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m
<VAR>R : Type u<VAR>M : Type v<VAR>Group R<VAR>MulAction R M<VAR>p : SubMulAction R M<GOAL>MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Group R<VAR>MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>MulAction.stabilizer R m = MulAction.stabilizer R ↑m
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : SubMulAction R M<VAR>h : (↑p).Nonempty<GOAL>0 ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : SubMulAction R M<VAR>x : M<VAR>hx : x ∈ p<GOAL>-x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : SubMulAction R M<VAR>x : M<GOAL>-x ∈ p ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : SubMulAction R M<VAR>x : ↥p<GOAL>↑(-x) = -↑x
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>GroupWithZero S<VAR>Monoid R<VAR>MulAction R M<VAR>SMul S R<VAR>MulAction S M<VAR>IsScalarTower S R M<VAR>p : SubMulAction R M<VAR>s : S<VAR>x : M<VAR>s0 : s ≠ 0<GOAL>s • x ∈ p ↔ x ∈ p
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s : SubMulAction M α<GOAL>s.inclusion.toFun = Subtype.val
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s : SubMulAction M α<GOAL>⇑s.inclusion = Subtype.val
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s : SubMulAction M α<GOAL>Set.range ⇑s.inclusion = s.carrier
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s : SubMulAction M α<GOAL>Function.Injective ⇑s.inclusion
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<GOAL>alternatingGroup α = Equiv.Perm.sign.ker
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<GOAL>f ∈ alternatingGroup α ↔ Equiv.Perm.sign f = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>l : List (Equiv.Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<GOAL>l.prod ∈ alternatingGroup α ↔ Even l.length
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>h : f.IsThreeCycle<GOAL>f ∈ alternatingGroup α
<VAR>n : ℕ<GOAL>finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>Nontrivial α<GOAL>2 * Fintype.card ↥(alternatingGroup α) = Fintype.card (Equiv.Perm α)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : ↥(alternatingGroup α)<VAR>hc : IsConj ↑σ ↑τ<VAR>hσ : (↑σ).support.card + 2 ≤ Fintype.card α<GOAL>IsConj σ τ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>h5 : 5 ≤ Fintype.card α<VAR>σ τ : ↥(alternatingGroup α)<VAR>hσ : (↑σ).IsThreeCycle<VAR>hτ : (↑τ).IsThreeCycle<GOAL>IsConj σ τ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<GOAL>Subgroup.closure {σ | σ.IsThreeCycle} = alternatingGroup α
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>h5 : 5 ≤ Fintype.card α<VAR>f : Equiv.Perm α<VAR>hf : f.IsThreeCycle<GOAL>Subgroup.normalClosure {⟨f, ⋯⟩} = ⊤
<VAR>g : Equiv.Perm (Fin 5)<VAR>h : 3 ∈ g.cycleType<GOAL>(g * g).IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>h3 : 3 ≤ Fintype.card α<GOAL>Nontrivial ↥(alternatingGroup α)
<GOAL>Subgroup.normalClosure {⟨finRotate 5, ⋯⟩} = ⊤
<GOAL>Subgroup.normalClosure {⟨Equiv.swap 0 4 * Equiv.swap 1 3, ⋯⟩} = ⊤
<VAR>g : Equiv.Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : ∀ n ∈ g.cycleType, n = 2<GOAL>IsConj (Equiv.swap 0 4 * Equiv.swap 1 3) g
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup G<VAR>AddAction G β<VAR>g : G<VAR>f : α ↪ β<GOAL>g +ᵥ f = f.trans (Equiv.toEmbedding (AddAction.toPerm g))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group G<VAR>MulAction G β<VAR>g : G<VAR>f : α ↪ β<GOAL>g • f = f.trans (Equiv.toEmbedding (MulAction.toPerm g))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup G<VAR>AddAction G β<VAR>g : G<VAR>f : α ↪ β<VAR>a : α<GOAL>(g +ᵥ f) a = g +ᵥ f a
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group G<VAR>MulAction G β<VAR>g : G<VAR>f : α ↪ β<VAR>a : α<GOAL>(g • f) a = g • f a
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group G<VAR>MulAction G β<VAR>g : G<VAR>f : α ↪ β<GOAL>⇑(g • f) = g • ⇑f
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup G<VAR>AddAction G β<VAR>g : G<VAR>f : α ↪ β<GOAL>⇑(g +ᵥ f) = g +ᵥ ⇑f
<VAR>M : Type u_1<VAR>Add M<VAR>self : AddCon M<VAR>w x y z : M<GOAL>Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)
<VAR>M : Type u_1<VAR>Mul M<VAR>self : Con M<VAR>w x y z : M<GOAL>Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<GOAL>Setoid.r = ⇑c
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<GOAL>Setoid.r = ⇑c
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>x : M<GOAL>c x x
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>x : M<GOAL>c x x
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>x y : M<GOAL>c x y → c y x
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>x y : M<GOAL>c x y → c y x
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>x y z : M<GOAL>c x y → c y z → c x z
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>x y z : M<GOAL>c x y → c y z → c x z
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<VAR>w x y z : M<GOAL>c w x → c y z → c (w * y) (x * z)
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<VAR>w x y z : M<GOAL>c w x → c y z → c (w + y) (x + z)
<VAR>M : Type u_1<VAR>Add M<VAR>s : Setoid M<VAR>h : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)<VAR>a b : M<GOAL>{ toSetoid := s, add' := h } a b ↔ Setoid.r a b
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Setoid M<VAR>h : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)<VAR>a b : M<GOAL>{ toSetoid := s, mul' := h } a b ↔ Setoid.r a b
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<VAR>H : ⇑c = ⇑d<GOAL>c = d
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<VAR>H : ⇑c = ⇑d<GOAL>c = d
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<VAR>H : ∀ (x y : M), c x y ↔ d x y<GOAL>c = d
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<VAR>H : ∀ (x y : M), c x y ↔ d x y<GOAL>c = d
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<VAR>H : c.toSetoid = d.toSetoid<GOAL>c = d
<VAR>M : Type u_1<VAR>Mul M<VAR>c d : Con M<VAR>H : c.toSetoid = d.toSetoid<GOAL>c = d
<VAR>M : Type u_1<VAR>Add M<VAR>c d : AddCon M<GOAL>c = d ↔ ∀ (x y : M), c x y ↔ d x y