ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>hm : m ∈ M<VAR>hn : n ∈ N<GOAL>m * n ∈ M * N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P : Submodule R A<GOAL>M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<GOAL>(M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>C : A → Prop<VAR>r : A<VAR>hr : r ∈ M * N<VAR>hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)<VAR>ha : ∀ (x y : A), C x → C y → C (x + y)<GOAL>C r
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>C : (r : A) → r ∈ M * N → Prop<VAR>mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯<VAR>r : A<VAR>hr : r ∈ M * N<GOAL>C r hr
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Set A<GOAL>Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<GOAL>M * ⊥ = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<GOAL>⊥ * M = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<GOAL>1 * M = M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<GOAL>M * 1 = M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P Q : Submodule R A<VAR>hmp : M ≤ P<VAR>hnq : N ≤ Q<GOAL>M * N ≤ P * Q
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P : Submodule R A<VAR>h : M ≤ N<GOAL>M * P ≤ N * P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P : Submodule R A<VAR>h : N ≤ P<GOAL>M * N ≤ M * P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P : Submodule R A<GOAL>M * (N ⊔ P) = M * N ⊔ M * P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N P : Submodule R A<GOAL>(M ⊔ N) * P = M * P ⊔ N * P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<GOAL>↑M * ↑N ⊆ ↑(M * N)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>A' : Type u_1<VAR>Semiring A'<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<GOAL>Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) N * Submodule.map (↑(MulOpposite.opLinearEquiv R)) M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R Aᵐᵒᵖ<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R Aᵐᵒᵖ<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M * N) = Submodule.comap (↑(MulOpposite.opLinearEquiv R)) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Semiring C<VAR>Algebra A B<VAR>Algebra A C<VAR>Algebra B C<VAR>IsScalarTower A B C<VAR>I J : Submodule B C<GOAL>Submodule.restrictScalars A (I * J) = Submodule.restrictScalars A I * Submodule.restrictScalars A J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Mul A<VAR>Module R A<VAR>S S' : Set A<VAR>x : A<VAR>hx : x ∈ Submodule.span R (S * S')<GOAL>∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ Submodule.span R (↑T * ↑T')
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>s t : Submodule R A<GOAL>s * t = Submodule.span R (↑s * ↑t)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>s : ι → Submodule R A<VAR>t : Submodule R A<GOAL>(⨆ i, s i) * t = ⨆ i, s i * t
<VAR>ι : Sort uι<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>t : Submodule R A<VAR>s : ι → Submodule R A<GOAL>t * ⨆ i, s i = ⨆ i, t * s i
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>P Q : Submodule R A<VAR>x : A<VAR>hx : x ∈ P * Q<GOAL>∃ T T', ↑T ⊆ ↑P ∧ ↑T' ⊆ ↑Q ∧ x ∈ Submodule.span R (↑T * ↑T')
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>P : Submodule R A<VAR>x y : A<GOAL>x ∈ Submodule.span R {y} * P ↔ ∃ z ∈ P, y * z = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>P : Submodule R A<VAR>x y : A<GOAL>x ∈ P * Submodule.span R {y} ↔ ∃ z ∈ P, z * y = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>p : Submodule R A<GOAL>Submodule.span R {x} * p = x • p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>Field S<VAR>Algebra R S<VAR>x : S<VAR>p : Submodule R S<VAR>y : S<VAR>hx : x ≠ 0<GOAL>y ∈ x • p ↔ x⁻¹ * y ∈ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>p : Submodule R S<VAR>y : S<VAR>hx : x ∈ nonZeroDivisors S<GOAL>x * y ∈ x • p ↔ y ∈ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>x y : R<GOAL>(x * y) • (M * N) = x • M * y • N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>n : ℕ<GOAL>Submodule.span R s ^ n = Submodule.span R (s ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<GOAL>M ^ n = Submodule.span R (↑M ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<GOAL>↑M ^ n ⊆ ↑(M ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>x : A<VAR>hx : x ∈ M<VAR>n : ℕ<GOAL>x ^ n ∈ M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<GOAL>M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯<VAR>n : ℕ<VAR>x : A<VAR>hx : x ∈ M ^ n<GOAL>C n x hx
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯<VAR>n : ℕ<VAR>x : A<VAR>hx : x ∈ M ^ n<GOAL>C n x hx
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>C : A → Prop<VAR>hr : ∀ (r : R), C ((algebraMap R A) r)<VAR>hadd : ∀ (x y : A), C x → C y → C (x + y)<VAR>hmul : ∀ m ∈ M, ∀ (x : A), C x → C (m * x)<VAR>x : A<VAR>n : ℕ<VAR>hx : x ∈ M ^ n<GOAL>C x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>C : A → Prop<VAR>hr : ∀ (r : R), C ((algebraMap R A) r)<VAR>hadd : ∀ (x y : A), C x → C y → C (x + y)<VAR>hmul : ∀ (x : A), C x → ∀ m ∈ M, C (x * m)<VAR>x : A<VAR>n : ℕ<VAR>hx : x ∈ M ^ n<GOAL>C x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>A' : Type u_1<VAR>Semiring A'<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<VAR>p : Submodule R A<GOAL>(Submodule.mapHom f) p = Submodule.map f.toLinearMap p
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>p : (Submodule R A)ᵐᵒᵖ<GOAL>Submodule.equivOpposite.symm p = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (MulOpposite.unop p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>p : Submodule R Aᵐᵒᵖ<GOAL>Submodule.equivOpposite p = MulOpposite.op (Submodule.comap (↑(MulOpposite.opLinearEquiv R)) p)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>A' : Type u_1<VAR>Semiring A'<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<VAR>n : ℕ<GOAL>Submodule.map f.toLinearMap (M ^ n) = Submodule.map f.toLinearMap M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : ℕ<VAR>M : Submodule R Aᵐᵒᵖ<GOAL>Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submodule R A<VAR>n : ℕ<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : ℕ<VAR>M : Submodule R Aᵐᵒᵖ<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>s : SetSemiring A<GOAL>Submodule.span.ringHom s = Submodule.span R (SetSemiring.down s)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>hm : m ∈ M<VAR>hn : n ∈ N<GOAL>n * m ∈ M * N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>M N : Submodule R A<GOAL>M * N = N * M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>M : ι → Set A<GOAL>∏ i ∈ s, Submodule.span R (M i) = Submodule.span R (∏ i ∈ s, M i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>x : ι → A<GOAL>∏ i ∈ s, Submodule.span R {x i} = Submodule.span R {∏ i ∈ s, x i}
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>s : SetSemiring A<VAR>P : Submodule R A<GOAL>s • P = Submodule.span R (SetSemiring.down s) * P
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>s t : SetSemiring A<VAR>M N : Submodule R A<VAR>h₁ : SetSemiring.down s ⊆ SetSemiring.down t<VAR>h₂ : M ≤ N<GOAL>s • M ≤ t • N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>a : A<VAR>M : Submodule R A<GOAL>Set.up {a} • M = Submodule.map (LinearMap.mulLeft R a) M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>x : A<VAR>I J : Submodule R A<GOAL>x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>x : A<VAR>I J : Submodule R A<GOAL>x ∈ I / J ↔ x • ↑J ⊆ ↑I
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>I J K : Submodule R A<GOAL>I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>I J K : Submodule R A<GOAL>I ≤ J / K ↔ I * K ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>I : Submodule R A<GOAL>1 ≤ 1 / I ↔ I ≤ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>I : Submodule R A<VAR>hI : I ≤ 1<GOAL>I ≤ I * (1 / I)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>I : Submodule R A<GOAL>I * (1 / I) ≤ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommSemiring A<VAR>Algebra R A<VAR>B : Type u_1<VAR>CommSemiring B<VAR>Algebra R B<VAR>I J : Submodule R A<VAR>h : A ≃ₐ[R] B<GOAL>Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : Rˣ<GOAL>∀ (a : R), (AddAut.mulLeft x) a = x • a
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : Rˣ<GOAL>∀ (a : R), (AddEquiv.symm (AddAut.mulLeft x)) a = x⁻¹ • a
<VAR>R : Type u_1<VAR>Semiring R<VAR>u : Rˣ<VAR>x : R<GOAL>(AddAut.mulRight u) x = x * ↑u
<VAR>R : Type u_1<VAR>Semiring R<VAR>u : Rˣ<VAR>x : R<GOAL>(AddEquiv.symm (AddAut.mulRight u)) x = x * ↑u⁻¹
<VAR>R : Type u_1<VAR>Mul R<VAR>Add R<VAR>Zero R<GOAL>∀ (a : R), isSumSq a ↔ a = 0 ∨ ∃ a_1 S, isSumSq S ∧ a = a_1 * a_1 + S
<VAR>R : Type u_1<VAR>Mul R<VAR>AddMonoid R<VAR>S1 S2 : R<VAR>p1 : isSumSq S1<VAR>p2 : isSumSq S2<GOAL>isSumSq (S1 + S2)
<VAR>R : Type u_1<VAR>Mul R<VAR>AddMonoid R<VAR>x : R<VAR>px : IsSquare x<GOAL>x ∈ SumSqIn R
<VAR>R : Type u_1<VAR>Mul R<VAR>AddMonoid R<GOAL>AddSubmonoid.closure IsSquare = SumSqIn R
<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>ExistsAddOfLE R<VAR>S : R<VAR>pS : isSumSq S<GOAL>0 ≤ S
<VAR>S : Type u_5<VAR>G : Type u_6<VAR>Inv G<VAR>SetLike S G<VAR>self : InvMemClass S G<VAR>s : S<VAR>x : G<GOAL>x ∈ s → x⁻¹ ∈ s
<VAR>S : Type u_5<VAR>G : Type u_6<VAR>Neg G<VAR>SetLike S G<VAR>self : NegMemClass S G<VAR>s : S<VAR>x : G<GOAL>x ∈ s → -x ∈ s
<VAR>S : Type u_5<VAR>G : Type u_6<VAR>InvolutiveInv G<GOAL>∀ {x : SetLike S G} [inst : InvMemClass S G] {H : S} {x_1 : G}, x_1⁻¹ ∈ H ↔ x_1 ∈ H
<VAR>S : Type u_5<VAR>G : Type u_6<VAR>InvolutiveNeg G<GOAL>∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, -x_1 ∈ H ↔ x_1 ∈ H
<VAR>M : Type u_5<VAR>S : Type u_6<VAR>DivInvMonoid M<VAR>SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H : S<VAR>x y : M<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x / y ∈ H
<VAR>M : Type u_5<VAR>S : Type u_6<VAR>SubNegMonoid M<VAR>SetLike S M<VAR>hSM : AddSubgroupClass S M<VAR>H : S<VAR>x y : M<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x - y ∈ H
<VAR>M : Type u_5<VAR>S : Type u_6<VAR>SubNegMonoid M<VAR>SetLike S M<VAR>hSM : AddSubgroupClass S M<VAR>K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℤ<GOAL>n • x ∈ K
<VAR>M : Type u_5<VAR>S : Type u_6<VAR>DivInvMonoid M<VAR>SetLike S M<VAR>hSM : SubgroupClass S M<VAR>K : S<VAR>x : M<VAR>hx : x ∈ K<VAR>n : ℤ<GOAL>x ^ n ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>a b : G<GOAL>a - b ∈ H ↔ b - a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>a b : G<GOAL>a / b ∈ H ↔ b / a ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>P : G → Prop<GOAL>(∃ x ∈ H, P (-x)) ↔ ∃ x ∈ H, P x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>P : G → Prop<GOAL>(∃ x ∈ H, P x⁻¹) ↔ ∃ x ∈ H, P x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<GOAL>y + x ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<GOAL>y * x ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<GOAL>x + y ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<GOAL>x * y ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x : ↥H<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x : ↥H<GOAL>↑(-x) = -↑x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>H K L : S<GOAL>↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>H K L : S<GOAL>↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x y : ↥H<GOAL>↑(x - y) = ↑x - ↑y
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x y : ↥H<GOAL>↑(x / y) = ↑x / ↑y
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<GOAL>⇑↑H = Subtype.val
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<GOAL>⇑↑H = Subtype.val
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x : ↥H<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x : ↥H<VAR>n : ℕ<GOAL>↑(n • x) = n • ↑x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x : ↥H<VAR>n : ℤ<GOAL>↑(n • x) = n • ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x : ↥H<VAR>n : ℤ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>x : ↥H<GOAL>(AddSubgroupClass.inclusion ⋯) x = x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>x : ↥H<GOAL>(SubgroupClass.inclusion ⋯) x = x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H K : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>h : H ≤ K<VAR>x : G<VAR>hx : x ∈ H<GOAL>(SubgroupClass.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H K : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>h : H ≤ K<VAR>x : G<VAR>hx : x ∈ H<GOAL>(AddSubgroupClass.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H K : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>h : H ≤ K<VAR>x : ↥K<VAR>hx : ↑x ∈ H<GOAL>(SubgroupClass.inclusion h) ⟨↑x, hx⟩ = x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>H K : S<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>h : H ≤ K<VAR>x : ↥K<VAR>hx : ↑x ∈ H<GOAL>(AddSubgroupClass.inclusion h) ⟨↑x, hx⟩ = x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>H K : S<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>L : S<VAR>hHK : H ≤ K<VAR>hKL : K ≤ L<VAR>x : ↥H<GOAL>(SubgroupClass.inclusion hKL) ((SubgroupClass.inclusion hHK) x) = (SubgroupClass.inclusion ⋯) x
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>H K : S<VAR>h : H ≤ K<VAR>a : ↥H<GOAL>↑((SubgroupClass.inclusion h) a) = ↑a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>H K : S<VAR>h : H ≤ K<VAR>a : ↥H<GOAL>↑((AddSubgroupClass.inclusion h) a) = ↑a
<VAR>G : Type u_1<VAR>Group G<VAR>S : Type u_6<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>H K : S<VAR>hH : H ≤ K<GOAL>(↑K).comp (SubgroupClass.inclusion hH) = ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Type u_6<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>H K : S<VAR>hH : H ≤ K<GOAL>(↑K).comp (AddSubgroupClass.inclusion hH) = ↑H
<VAR>G : Type u_5<VAR>Group G<VAR>self : Subgroup G<VAR>x : G<GOAL>x ∈ self.carrier → x⁻¹ ∈ self.carrier
<VAR>G : Type u_5<VAR>AddGroup G<VAR>self : AddSubgroup G<VAR>x : G<GOAL>x ∈ self.carrier → -x ∈ self.carrier
<VAR>G : Type u_1<VAR>Group G<VAR>s : Subgroup G<VAR>x : G<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : AddSubgroup G<VAR>x : G<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>x : G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s<VAR>h_mul : s 1<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier<GOAL>x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } ↔ x ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>x : G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s<VAR>h_mul : s 0<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier<GOAL>x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } ↔ x ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s<VAR>h_mul : s 0<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier<GOAL>↑{ carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } = s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s<VAR>h_mul : s 1<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier<GOAL>↑{ carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s<VAR>h_mul : s 0<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier<VAR>h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a + b ∈ t<VAR>h_mul' : t 0<VAR>h_inv' : ∀ {x : G}, x ∈ { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier → -x ∈ { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier<GOAL>{ carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } ≤ { carrier := t, add_mem' := h_one', zero_mem' := h_mul', neg_mem' := h_inv' } ↔ s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s<VAR>h_mul : s 1<VAR>h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier<VAR>h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a * b ∈ t<VAR>h_mul' : t 1<VAR>h_inv' : ∀ {x : G}, x ∈ { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrier → x⁻¹ ∈ { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrier<GOAL>{ carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } ≤ { carrier := t, mul_mem' := h_one', one_mem' := h_mul', inv_mem' := h_inv' } ↔ s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<GOAL>↑K.toSubmonoid = ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<GOAL>↑K.toAddSubmonoid = ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>x : G<GOAL>x ∈ K.toSubmonoid ↔ x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>x : G<GOAL>x ∈ K.toAddSubmonoid ↔ x ∈ K
<VAR>G : Type u_1<VAR>Group G<GOAL>Function.Injective Subgroup.toSubmonoid
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Function.Injective AddSubgroup.toAddSubmonoid
<VAR>G : Type u_1<VAR>AddGroup G<VAR>p q : AddSubgroup G<GOAL>p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q
<VAR>G : Type u_1<VAR>Group G<VAR>p q : Subgroup G<GOAL>p.toSubmonoid = q.toSubmonoid ↔ p = q
<VAR>G : Type u_1<VAR>Group G<GOAL>StrictMono Subgroup.toSubmonoid