ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>p : Submodule R₂ M₂<GOAL>(Submodule.orderIsoMapComap e).symm p = Submodule.map e.symm p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f₁ f₂ : M →ₛₗ[τ₁₂] M₂<GOAL>Submodule.comap f₁ q ⊓ Submodule.comap f₂ q ≤ Submodule.comap (f₁ + f₂) q
<VAR>R : Type u_1<VAR>N : Type u_9<VAR>N₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid N<VAR>AddCommMonoid N₂<VAR>Module R N<VAR>Module R N₂<VAR>qₗ : Submodule R N₂<VAR>fₗ : N →ₗ[R] N₂<VAR>c : R<GOAL>Submodule.comap fₗ qₗ ≤ Submodule.comap (c • fₗ) qₗ
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>↑((f.submoduleMap p) x) = f ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<GOAL>Function.Surjective ⇑(f.submoduleMap p)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomSurjective σ₂₁<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[σ₂₁] M<VAR>h : ∀ (c : M₂), f c ∈ p<VAR>p' : Submodule R₂ M₂<GOAL>Submodule.map (LinearMap.codRestrict p f h) p' = Submodule.comap p.subtype (Submodule.map f p')
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>σ₂₁ : R₂ →+* R<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[σ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<VAR>p' : Submodule R ↥p<GOAL>Submodule.comap (LinearMap.codRestrict p f hf) p' = Submodule.comap f (Submodule.map p.subtype p')
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<GOAL>Submodule.map (↑e) p = Submodule.comap (↑e.symm) p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>↑((e.submoduleMap p) x) = e ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<VAR>x : ↥(Submodule.map (↑e) p)<GOAL>↑((e.submoduleMap p).symm x) = e.symm ↑x
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a a' : R<VAR>CommRing R<GOAL>MvPolynomial.C (a - a') = MvPolynomial.C a - MvPolynomial.C a'
<VAR>R : Type u<VAR>σ : Type u_1<VAR>a : R<VAR>CommRing R<GOAL>MvPolynomial.C (-a) = -MvPolynomial.C a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>m : σ →₀ ℕ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (-p) = -MvPolynomial.coeff m p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>m : σ →₀ ℕ<VAR>p q : MvPolynomial σ R<GOAL>MvPolynomial.coeff m (p - q) = MvPolynomial.coeff m p - MvPolynomial.coeff m q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<GOAL>(-p).support = p.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p - q).support ⊆ p.support ∪ q.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<GOAL>(-p).degrees = p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p - q).degrees ≤ p.degrees ⊔ q.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<GOAL>(-p).vars = p.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>q : MvPolynomial σ R<VAR>DecidableEq σ<GOAL>(p - q).vars ⊆ p.vars ∪ q.vars
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>q : MvPolynomial σ R<VAR>DecidableEq σ<VAR>hpq : Disjoint p.vars q.vars<GOAL>(p - q).vars = p.vars ∪ q.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>q : MvPolynomial σ R<VAR>CommRing S<VAR>f : R →+* S<VAR>g : σ → S<GOAL>MvPolynomial.eval₂ f g (p - q) = MvPolynomial.eval₂ f g p - MvPolynomial.eval₂ f g q
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>q : MvPolynomial σ R<VAR>f : σ → R<GOAL>(MvPolynomial.eval f) (p - q) = (MvPolynomial.eval f) p - (MvPolynomial.eval f) q
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>CommRing S<VAR>f : R →+* S<VAR>g : σ → S<GOAL>MvPolynomial.eval₂ f g (-p) = -MvPolynomial.eval₂ f g p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>f : σ → R<GOAL>(MvPolynomial.eval f) (-p) = -(MvPolynomial.eval f) p
<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommRing S<VAR>f : MvPolynomial σ ℤ →+* S<VAR>n : ℤ<GOAL>f (MvPolynomial.C n) = ↑n
<VAR>S : Type v<VAR>CommRing S<VAR>R : Type u<VAR>c : ℤ →+* S<VAR>f : MvPolynomial R ℤ →+* S<VAR>x : MvPolynomial R ℤ<GOAL>MvPolynomial.eval₂ c (⇑f ∘ MvPolynomial.X) x = f x
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>x : σ<VAR>f g : MvPolynomial σ R<VAR>k : ℕ<VAR>h : 0 < k<VAR>hf : ∀ m ∈ f.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g<VAR>hg : ∀ m ∈ g.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g<GOAL>MvPolynomial.degreeOf x (f - g) < k
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>a : MvPolynomial σ R<GOAL>(-a).totalDegree = a.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>a b : MvPolynomial σ R<GOAL>(a - b).totalDegree ≤ max a.totalDegree b.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommRing R<VAR>p : MvPolynomial σ R<VAR>r : R<GOAL>(p - MvPolynomial.C r).totalDegree ≤ p.totalDegree
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<VAR>s' : σ →₀ ℕ<GOAL>MvPolynomial.coeff s' (x.divMonomial s) = MvPolynomial.coeff (s + s') x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>(x.divMonomial s).support = x.support.preimage (fun x => s + x) ⋯
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<GOAL>MvPolynomial.divMonomial 0 s = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<GOAL>x.divMonomial 0 = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x y : MvPolynomial σ R<VAR>s : σ →₀ ℕ<GOAL>(x + y).divMonomial s = x.divMonomial s + y.divMonomial s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a b : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>x.divMonomial (a + b) = (x.divMonomial a).divMonomial b
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>((MvPolynomial.monomial a) 1 * x).divMonomial a = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>(x * (MvPolynomial.monomial a) 1).divMonomial a = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a : σ →₀ ℕ<GOAL>((MvPolynomial.monomial a) 1).divMonomial a = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s' s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<VAR>h : ¬s ≤ s'<GOAL>MvPolynomial.coeff s' (x.modMonomial s) = MvPolynomial.coeff s' x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s' s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<VAR>h : s ≤ s'<GOAL>MvPolynomial.coeff s' (x.modMonomial s) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>((MvPolynomial.monomial s) 1 * x).modMonomial s = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>(x * (MvPolynomial.monomial s) 1).modMonomial s = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<GOAL>((MvPolynomial.monomial s) 1).modMonomial s = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : σ →₀ ℕ<GOAL>(MvPolynomial.monomial s) 1 * x.divMonomial s + x.modMonomial s = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : σ →₀ ℕ<GOAL>x.modMonomial s + (MvPolynomial.monomial s) 1 * x.divMonomial s = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ →₀ ℕ<VAR>x : MvPolynomial σ R<GOAL>(MvPolynomial.monomial i) 1 ∣ x ↔ x.modMonomial i = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>(MvPolynomial.X i * x).divMonomial (Finsupp.single i 1) = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.X i).divMonomial (Finsupp.single i 1) = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>(x * MvPolynomial.X i).divMonomial (Finsupp.single i 1) = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>(MvPolynomial.X i * x).modMonomial (Finsupp.single i 1) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>(x * MvPolynomial.X i).modMonomial (Finsupp.single i 1) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.X i).modMonomial (Finsupp.single i 1) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>MvPolynomial.X i * x.divMonomial (Finsupp.single i 1) + x.modMonomial (Finsupp.single i 1) = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>x.modMonomial (Finsupp.single i 1) + MvPolynomial.X i * x.divMonomial (Finsupp.single i 1) = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>MvPolynomial.X i ∣ x ↔ x.modMonomial (Finsupp.single i 1) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>r s : R<VAR>i j : σ →₀ ℕ<GOAL>(MvPolynomial.monomial i) r ∣ (MvPolynomial.monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Nontrivial R<VAR>i j : σ →₀ ℕ<GOAL>(MvPolynomial.monomial i) 1 ∣ (MvPolynomial.monomial j) 1 ↔ i ≤ j
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Nontrivial R<VAR>i j : σ<GOAL>MvPolynomial.X i ∣ MvPolynomial.X j ↔ i = j
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>i : σ<VAR>j : σ →₀ ℕ<VAR>r : R<GOAL>MvPolynomial.X i ∣ (MvPolynomial.monomial j) r ↔ r = 0 ∨ j i ≠ 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>LieRingModule L M₁<VAR>LieModule R L M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>LieRingModule L M₃<VAR>LieModule R L M₃<VAR>g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<GOAL>LinearMap.range (↑g ∘ₗ TensorProduct.mapIncl (((LieModule.toEnd R L M₁) x).maxGenEigenspace χ₁) (((LieModule.toEnd R L M₂) x).maxGenEigenspace χ₂)) ≤ ((LieModule.toEnd R L M₃) x).maxGenEigenspace (χ₁ + χ₂)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ : R<VAR>x y : L<VAR>m : M<VAR>hy : y ∈ ((LieModule.toEnd R L L) x).maxGenEigenspace χ₁<VAR>hm : m ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace χ₂<GOAL>⁅y, m⁆ ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace (χ₁ + χ₂)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : R<VAR>x : L<VAR>m : M<GOAL>m ∈ LieModule.weightSpaceOf M χ x ↔ ∃ k, (((LieModule.toEnd R L M) x - χ • 1) ^ k) m = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<GOAL>↑(LieModule.weightSpaceOf M 0 x) = ⨆ k, LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : L → R<VAR>m : M<GOAL>m ∈ LieModule.weightSpace M χ ↔ ∀ (x : L), ∃ k, (((LieModule.toEnd R L M) x - χ x • 1) ^ k) m = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<VAR>χ : L → R<GOAL>LieModule.weightSpace M χ ≤ LieModule.weightSpaceOf M (χ x) x
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>self : LieModule.Weight R L M<GOAL>LieModule.weightSpace M self.toFun ≠ ⊥
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : L → R<VAR>h : LieModule.weightSpace M χ ≠ ⊥<GOAL>⇑{ toFun := χ, weightSpace_ne_bot' := h } = χ
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<GOAL>LieModule.weightSpace M ⇑χ ≠ ⊥
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ : LieModule.Weight R L M<VAR>h : ∀ (x : L), χ₁ x = χ₂ x<GOAL>χ₁ = χ₂
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ : LieModule.Weight R L M<GOAL>χ₁ = χ₂ ↔ ⇑χ₁ = ⇑χ₂
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<GOAL>∃ x ∈ LieModule.weightSpace M ⇑χ, x ≠ 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Nontrivial ↥↑(LieModule.weightSpace M 0)<GOAL>⇑0 = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Nontrivial ↥↑(LieModule.weightSpace M 0)<VAR>x : L<GOAL>0 x = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<VAR>hχ : χ.IsZero<GOAL>⇑χ = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<GOAL>⇑χ = 0 ↔ χ.IsZero
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Nontrivial ↥↑(LieModule.weightSpace M 0)<VAR>χ : LieModule.Weight R L M<GOAL>χ.IsZero ↔ χ = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Nontrivial ↥↑(LieModule.weightSpace M 0)<GOAL>LieModule.Weight.IsZero 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Nontrivial ↥↑(LieModule.weightSpace M 0)<VAR>χ : LieModule.Weight R L M<GOAL>χ.IsNonZero ↔ χ ≠ 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<VAR>x : L<GOAL>LieModule.weightSpaceOf M (χ x) x ≠ ⊥
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : LieModule.Weight R L M<VAR>x : L<GOAL>((LieModule.toEnd R L M) x).HasEigenvalue (χ x)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>NoZeroSMulDivisors R M<VAR>IsReduced R<VAR>x : L<VAR>h : IsNilpotent ((LieModule.toEnd R L M) x)<VAR>χ : LieModule.Weight R L M<GOAL>χ x = 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieModule.IsNilpotent R L M<GOAL>LieModule.weightSpace M 0 = ⊤
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ : L → R<GOAL>↑(LieModule.weightSpace M (χ ∘ ⇑⊤.incl)) = ↑(LieModule.weightSpace M χ)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>χ : L → R<VAR>x : L<GOAL>∃ k, ↑(LieModule.weightSpace M χ) ≤ LinearMap.ker (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>x : L<GOAL>∃ k, ↑(LieModule.weightSpace M 0) ≤ LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>χ : L → R<VAR>x : L<GOAL>IsNilpotent ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(LieModule.weightSpace M χ))) (χ x))
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>x : L<GOAL>IsNilpotent ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M 0)) x)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>(LieModule.weightSpace M 0).normalizer = LieModule.weightSpace M 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>⨆ k, LieSubmodule.ucs k ⊥ ≤ LieModule.weightSpace M 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<GOAL>⨆ k, LieSubmodule.ucs k ⊥ = LieModule.weightSpace M 0
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<VAR>m : M<GOAL>m ∈ LieModule.posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, ((LieModule.toEnd R L M) x ^ k) n = m
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<VAR>k : ℕ<GOAL>LieModule.posFittingCompOf R M x ≤ LieModule.lowerCentralSeries R L M k
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieModule.IsNilpotent R L M<VAR>x : L<GOAL>LieModule.posFittingCompOf R M x = ⊥
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>m : M<GOAL>m ∈ LieModule.posFittingComp R L M ↔ m ∈ ⨆ x, LieModule.posFittingCompOf R M x
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : L<GOAL>LieModule.posFittingCompOf R M x ≤ LieModule.posFittingComp R L M
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<GOAL>LieModule.posFittingComp R L M ≤ ⨅ k, LieModule.lowerCentralSeries R L M k
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>IsNoetherian R M<VAR>IsArtinian R M<GOAL>⨅ k, LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>LieModule.IsNilpotent R L M<GOAL>LieModule.posFittingComp R L M = ⊥
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f (LieModule.posFittingComp R L M) ≤ LieModule.posFittingComp R L M₂
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>M₂ : Type u_5<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f (LieModule.weightSpace M χ) ≤ LieModule.weightSpace M₂ χ