ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a * c ∣ b * c ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a b : α<VAR>hd : a ∣ b<VAR>hnd : ¬b ∣ a<GOAL>DvdNotUnit a b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>x : α<GOAL>IsRelPrime 0 x ↔ IsUnit x
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>x : α<GOAL>IsRelPrime x 0 ↔ IsUnit x
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>Nontrivial α<GOAL>¬IsRelPrime 0 0
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>x y : α<VAR>Nontrivial α<VAR>h : IsRelPrime x y<GOAL>x ≠ 0 ∨ y ≠ 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>x y : α<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>x y : α<GOAL>x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>p q : α<VAR>h₁ : q ≠ 0<VAR>h₂ : p ∣ q<GOAL>p ≠ 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<GOAL>IsPrimal 0
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>m n : α<VAR>hm : IsPrimal m<VAR>hn : IsPrimal n<GOAL>IsPrimal (m * n)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : α<VAR>Subsingleton αˣ<GOAL>a ∣ b → b ∣ a → a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : α<VAR>Subsingleton αˣ<GOAL>a ∣ b → b ∣ a → b = a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : α<VAR>Subsingleton αˣ<VAR>h : ∀ (c : α), a ∣ c ↔ b ∣ c<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : α<VAR>Subsingleton αˣ<VAR>h : ∀ (c : α), c ∣ a ↔ c ∣ b<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a : α<VAR>m n : ℕ<VAR>ha₀ : a ≠ 0<VAR>ha : ¬IsUnit a<GOAL>a ^ n ∣ a ^ m ↔ n ≤ m
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>s : Set ι<VAR>f g : ι → M₀<GOAL>(s.indicator fun i => f i * g i) = fun i => s.indicator f i * s.indicator g i
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>i : ι<VAR>s : Set ι<VAR>f g : ι → M₀<GOAL>s.indicator (fun j => f j * g j) i = s.indicator f i * g i
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>i : ι<VAR>s : Set ι<VAR>f g : ι → M₀<GOAL>s.indicator (fun j => f j * g j) i = f i * s.indicator g i
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>s t : Set ι<VAR>f g : ι → M₀<VAR>i : ι<GOAL>(s ∩ t).indicator (fun j => f j * g j) i = s.indicator f i * t.indicator g i
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroOneClass M₀<VAR>s t : Set ι<GOAL>(s ∩ t).indicator 1 = s.indicator 1 * t.indicator 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M₀ : Type u_4<VAR>MulZeroOneClass M₀<VAR>s : Set ι<VAR>i : ι<VAR>t : Set κ<VAR>j : κ<GOAL>(s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroOneClass M₀<VAR>s : Set ι<VAR>i : ι<VAR>Nontrivial M₀<GOAL>s.indicator 1 i = 0 ↔ i ∉ s
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroOneClass M₀<VAR>s : Set ι<VAR>i : ι<VAR>Nontrivial M₀<GOAL>s.indicator 1 i = 1 ↔ i ∈ s
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroOneClass M₀<VAR>s t : Set ι<VAR>Nontrivial M₀<VAR>h : s.indicator 1 = t.indicator 1<GOAL>s = t
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>Zero R<VAR>One R<VAR>NeZero 1<GOAL>Function.support 1 = Set.univ
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>Zero R<VAR>One R<VAR>NeZero 1<GOAL>Function.mulSupport 0 = Set.univ
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>f g : ι → M₀<GOAL>(Function.support fun x => f x * g x) ⊆ Function.support f
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>f g : ι → M₀<GOAL>(Function.support fun x => f x * g x) ⊆ Function.support g
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>f g : ι → M₀<GOAL>(Function.support fun x => f x * g x) = Function.support f ∩ Function.support g
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>f g : ι → M₀<GOAL>Function.support (f * g) = Function.support f ∩ Function.support g
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>NoZeroDivisors M₀<VAR>n : ℕ<VAR>f : ι → M₀<VAR>hn : n ≠ 0<GOAL>(Function.support fun a => f a ^ n) = Function.support f
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>NoZeroDivisors M₀<VAR>n : ℕ<VAR>f : ι → M₀<VAR>hn : n ≠ 0<GOAL>Function.support (f ^ n) = Function.support f
<VAR>ι : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>f : ι → G₀<GOAL>(Function.support fun a => (f a)⁻¹) = Function.support f
<VAR>ι : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>f : ι → G₀<GOAL>Function.support f⁻¹ = Function.support f
<VAR>ι : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>f g : ι → G₀<GOAL>(Function.support fun a => f a / g a) = Function.support f ∩ Function.support g
<VAR>ι : Type u_1<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>f g : ι → G₀<GOAL>Function.support (f / g) = Function.support f ∩ Function.support g
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddLeftCancelMonoid R<VAR>f : ι → R<GOAL>(Function.mulSupport fun x => 1 + f x) = Function.support f
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddLeftCancelMonoid R<VAR>f : ι → R<GOAL>Function.mulSupport (1 + f) = Function.support f
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddRightCancelMonoid R<VAR>f : ι → R<GOAL>(Function.mulSupport fun x => f x + 1) = Function.support f
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddRightCancelMonoid R<VAR>f : ι → R<GOAL>Function.mulSupport (f + 1) = Function.support f
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddGroup R<VAR>f : ι → R<GOAL>Function.mulSupport (1 - f) = Function.support f
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>One R<VAR>AddGroup R<VAR>f : ι → R<GOAL>(Function.mulSupport fun x => 1 - f x) = Function.support f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.lcs 0 N = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.lcs (k + 1) N = ⁅⊤, LieSubmodule.lcs k N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>LieSubmodule.lcs k (N₁ ⊔ N₂) = LieSubmodule.lcs k N₁ ⊔ LieSubmodule.lcs k N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieModule.lowerCentralSeries R L M 0 = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<GOAL>LieModule.lowerCentralSeries R L M (k + 1) = ⁅⊤, LieModule.lowerCentralSeries R L M k⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.lcs k N ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>LieModule.lowerCentralSeries R L (↥↑N) k = LieSubmodule.comap N.incl (LieSubmodule.lcs k N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.map N.incl (LieModule.lowerCentralSeries R L (↥↑N) k) = LieSubmodule.lcs k N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>Antitone (LieModule.lowerCentralSeries R L M)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>IsArtinian R M<GOAL>∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, LieModule.lowerCentralSeries R L M k = LieModule.lowerCentralSeries R L M l
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieModule.IsTrivial L M ↔ LieModule.lowerCentralSeries R L M 1 = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>x : L<VAR>m : M<VAR>k : ℕ<GOAL>(⇑((LieModule.toEnd R L M) x))^[k] m ∈ LieModule.lowerCentralSeries R L M k
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>x y : L<VAR>m : M<VAR>k : ℕ<GOAL>(⇑((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y))^[k] m ∈ LieModule.lowerCentralSeries R L M (2 * k)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>M₂ : Type w₁<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.lowerCentralSeries R L M k) ≤ LieModule.lowerCentralSeries R L M₂ k
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>M₂ : Type w₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Function.Surjective ⇑f<GOAL>LieSubmodule.map f (LieModule.lowerCentralSeries R L M k) = LieModule.lowerCentralSeries R L M₂ k
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>k : ℕ<GOAL>LieAlgebra.derivedSeries R L k ≤ LieModule.lowerCentralSeries R L L k
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>self : LieModule.IsNilpotent R L M<GOAL>∃ k, LieModule.lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule.IsNilpotent R L M<GOAL>∃ k, LieModule.lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule.IsNilpotent R L M<GOAL>⨅ k, LieModule.lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieModule.IsNilpotent R L M ↔ ∃ k, LieModule.lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>LieModule.IsNilpotent R L ↥↑N ↔ ∃ k, LieSubmodule.lcs k N = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>hM : LieModule.IsNilpotent R L M<GOAL>∃ k, ∀ (x : L), (LieModule.toEnd R L M) x ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>LieModule.IsNilpotent R L M<VAR>x : L<GOAL>IsNilpotent ((LieModule.toEnd R L M) x)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>LieModule.IsNilpotent R L M<VAR>x y : L<GOAL>IsNilpotent ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>LieModule.IsNilpotent R L M<VAR>x : L<GOAL>((LieModule.toEnd R L M) x).maxGenEigenspace 0 = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>h₁ : N ≤ LieModule.maxTrivSubmodule R L M<VAR>h₂ : LieModule.IsNilpotent R L (M ⧸ N)<GOAL>LieModule.IsNilpotent R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>LieModule.IsNilpotent R L (M ⧸ N) ↔ ∃ k, LieModule.lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>h : LieModule.IsNilpotent R L (M ⧸ N)<GOAL>⨅ k, LieModule.lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule.IsNilpotent R L M<GOAL>LieModule.nilpotencyLength R L M = 0 ↔ Subsingleton M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<GOAL>LieModule.nilpotencyLength R L M = k + 1 ↔ LieModule.lowerCentralSeries R L M (k + 1) = ⊥ ∧ LieModule.lowerCentralSeries R L M k ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Nontrivial M<GOAL>LieModule.nilpotencyLength R L M = 1 ↔ LieModule.IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule.IsNilpotent R L M<VAR>h : LieModule.nilpotencyLength R L M ≤ 1<GOAL>LieModule.IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieModule.lowerCentralSeriesLast R L M ≤ LieModule.maxTrivSubmodule R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>Nontrivial M<VAR>LieModule.IsNilpotent R L M<GOAL>Nontrivial ↥↑(LieModule.lowerCentralSeriesLast R L M)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule.IsNilpotent R L M<VAR>h : ¬LieModule.IsTrivial L M<GOAL>LieModule.lowerCentralSeriesLast R L M ≤ LieModule.lowerCentralSeries R L M 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>LieModule.IsNilpotent R L M<GOAL>Disjoint (LieModule.lowerCentralSeries R L M 1) (LieModule.maxTrivSubmodule R L M) ↔ LieModule.IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>Nontrivial M<VAR>LieModule.IsNilpotent R L M<GOAL>Nontrivial ↥↑(LieModule.maxTrivSubmodule R L M)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<GOAL>↑(LieModule.lowerCentralSeries R (↥(LieModule.toEnd R L M).range) M k) = ↑(LieModule.lowerCentralSeries R L M k)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieModule.IsNilpotent R (↥(LieModule.toEnd R L M).range) M ↔ LieModule.IsNilpotent R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>LieSubmodule.ucs 0 N = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>k : ℕ<GOAL>LieSubmodule.ucs (k + 1) N = (LieSubmodule.ucs k N).normalizer
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>k l : ℕ<GOAL>LieSubmodule.ucs (k + l) N = LieSubmodule.ucs k (LieSubmodule.ucs l N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<VAR>h : N₁ ≤ N₂<GOAL>LieSubmodule.ucs k N₁ ≤ LieSubmodule.ucs k N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N₁ : LieSubmodule R L M<VAR>h : N₁.normalizer = N₁<VAR>k : ℕ<GOAL>LieSubmodule.ucs k N₁ = N₁
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N₁ : LieSubmodule R L M<VAR>h : N₁.normalizer = N₁<VAR>k : ℕ<GOAL>LieSubmodule.ucs k ⊥ ≤ N₁
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N₁ N₂ : LieSubmodule R L M<VAR>l k : ℕ<GOAL>LieSubmodule.lcs (l + k) N₁ ≤ N₂ ↔ LieSubmodule.lcs l N₁ ≤ LieSubmodule.ucs k N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>LieSubmodule.lcs k N₁ ≤ N₂ ↔ N₁ ≤ LieSubmodule.ucs k N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<GOAL>GaloisConnection (fun N => LieSubmodule.lcs k N) fun N => LieSubmodule.ucs k N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>k : ℕ<GOAL>LieSubmodule.ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieModule.IsNilpotent R L M ↔ ∃ k, LieSubmodule.ucs k ⊥ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<VAR>k : ℕ<GOAL>LieSubmodule.comap N.incl (LieSubmodule.ucs k ⊥) = LieSubmodule.ucs k ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N : LieSubmodule R L M<GOAL>LieModule.IsNilpotent R L ↥↑N ↔ ∃ k, N ≤ LieSubmodule.ucs k ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieSubmodule.ucs 1 ⊥ = LieModule.maxTrivSubmodule R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L₂ M₂<VAR>LieModule R L₂ M₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>g : M →ₗ[R] M₂<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<VAR>k : ℕ<GOAL>Submodule.map g ↑(LieModule.lowerCentralSeries R L M k) = ↑(LieModule.lowerCentralSeries R L₂ M₂ k)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L₂ M₂<VAR>LieModule R L₂ M₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>g : M →ₗ[R] M₂<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<VAR>LieModule.IsNilpotent R L M<GOAL>LieModule.IsNilpotent R L₂ M₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>L₂ : Type u_1<VAR>M₂ : Type u_2<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L₂ M₂<VAR>LieModule R L₂ M₂<VAR>f : L ≃ₗ⁅R⁆ L₂<VAR>g : M ≃ₗ[R] M₂<VAR>hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆<GOAL>LieModule.IsNilpotent R L M ↔ LieModule.IsNilpotent R L₂ M₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieModule.IsNilpotent R (↥⊤) M ↔ LieModule.IsNilpotent R L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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<GOAL>LieModule.IsNilpotent R L ↥⊤ ↔ LieModule.IsNilpotent R L M
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<GOAL>∃ k, ∀ (x : L), (LieAlgebra.ad R L) x ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>↑(LieModule.lowerCentralSeries R L (L ⧸ I) k) = ↑(LieModule.lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>↑(LieModule.lowerCentralSeries R (↥↑I) (↥↑I) k) ≤ ↑(LieModule.lowerCentralSeries R L (↥↑I) k)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>h₁ : I ≤ LieAlgebra.center R L<VAR>h₂ : LieAlgebra.IsNilpotent R (L ⧸ I)<GOAL>LieAlgebra.IsNilpotent R L
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>Nontrivial L<VAR>LieAlgebra.IsNilpotent R L<GOAL>Nontrivial ↥↑(LieAlgebra.center R L)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>k : ℕ<VAR>f : L →ₗ⁅R⁆ L'<GOAL>LieIdeal.map f (LieModule.lowerCentralSeries R L L k) ≤ LieModule.lowerCentralSeries R L' L' k
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>k : ℕ<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : Function.Surjective ⇑f<GOAL>LieIdeal.map f (LieModule.lowerCentralSeries R L L k) = LieModule.lowerCentralSeries R L' L' k
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>h₁ : LieAlgebra.IsNilpotent R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Function.Injective ⇑f<GOAL>LieAlgebra.IsNilpotent R L
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>h₁ : LieAlgebra.IsNilpotent R L<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Function.Surjective ⇑f<GOAL>LieAlgebra.IsNilpotent R L'
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>e : L ≃ₗ⁅R⁆ L'<GOAL>LieAlgebra.IsNilpotent R L ↔ LieAlgebra.IsNilpotent R L'
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>LieAlgebra.IsNilpotent R L<VAR>f : L →ₗ⁅R⁆ L'<GOAL>LieAlgebra.IsNilpotent R ↥f.range