ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>N : LieSubmodule R L M<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>N ≤ LieSubmodule.comap f (LieSubmodule.map f N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>N : LieSubmodule R L M<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : f.ker = ⊥<GOAL>LieSubmodule.comap f (LieSubmodule.map f N) = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>AddCommGroup M₂<VAR>Module R M₂<VAR>LieRingModule L M₂<VAR>LieModule R L M₂<VAR>I : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf₁ : f.ker = ⊥<VAR>hf₂ : N₂ ≤ f.range<GOAL>LieSubmodule.comap f ⁅I, N₂⁆ = ⁅I, LieSubmodule.comap f N₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>LieSubmodule.map N.incl (LieSubmodule.comap N.incl N') = N ⊓ N'
<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>f : L →ₗ⁅R⁆ L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>LieIdeal.map f ⁅I₁, I₂⁆ ≤ ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
<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>f : L →ₗ⁅R⁆ L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>LieIdeal.map f ⁅I₁, I₂⁆ = ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
<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>f : L →ₗ⁅R⁆ L'<VAR>J₁ J₂ : LieIdeal R L'<GOAL>⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ≤ LieIdeal.comap f ⁅J₁, J₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I₁ I₂ : LieIdeal R L<GOAL>LieIdeal.map I₁.incl (LieIdeal.comap I₁.incl I₂) = I₁ ⊓ I₂
<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>f : L →ₗ⁅R⁆ L'<VAR>J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>LieIdeal.comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ⊔ f.ker
<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>f : L →ₗ⁅R⁆ L'<VAR>J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>LieIdeal.map f ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>I₁ I₂ : LieIdeal R L<GOAL>⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>I₁ I₂ : LieIdeal R L<VAR>h₁ : I₁ ≤ I<VAR>h₂ : I₂ ≤ I<GOAL>⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I₁, I₂⁆
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x : α i<VAR>j : ι<GOAL>(MulHom.single i) x j = Pi.single i x j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x y : α i<GOAL>Pi.single i (x * y) = Pi.single i x * Pi.single i y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>a : α i<VAR>f : (i : ι) → α i<GOAL>Pi.single i (a * f i) j = Pi.single i a j * f j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i j : ι<VAR>f : (i : ι) → α i<VAR>a : α i<GOAL>Pi.single i (f i * a) j = f j * Pi.single i a j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (i : ι) → α i<VAR>a : α i<GOAL>Pi.single i (a * f i) = Pi.single i a * f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MulZeroClass (α i)<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (i : ι) → α i<VAR>a : α i<GOAL>Pi.single i (f i * a) = f * Pi.single i a
<VAR>M : Type u_1<VAR>β : Type u_4<VAR>SMul M β<VAR>α : Type u_5<VAR>Monoid M<VAR>AddMonoid α<VAR>DistribMulAction M α<VAR>a : M<VAR>c : β<GOAL>a • (0, c) = (0, a • c)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>SMul M α<VAR>β : Type u_5<VAR>Monoid M<VAR>AddMonoid β<VAR>DistribMulAction M β<VAR>a : M<VAR>b : α<GOAL>a • (b, 0) = (a • b, 0)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>FunLike F α β<VAR>ZeroHomClass F α β<VAR>a : α<VAR>f : F<VAR>neZero : NeZero (f a)<GOAL>NeZero a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>FunLike F α β<VAR>ZeroHomClass F α β<VAR>a : α<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>NeZero a<GOAL>NeZero (f a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>FunLike F α β<VAR>MonoidWithZeroHomClass F α β<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : ZeroHom α β<VAR>h1 : f.toFun 1 = 1<VAR>hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y<GOAL>⇑{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>(↑↑f).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f g : α →*₀ β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<VAR>h1 : (↑f).toFun 1 = 1<VAR>hmul : ∀ (x y : α), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y<GOAL>{ toZeroHom := ↑f, map_one' := h1, map_mul' := hmul } = f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : MulZeroOneClass α} {x_1 : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : MulZeroOneClass α} {x_1 : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>f 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>f 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<VAR>a b : α<GOAL>f (a * b) = f a * f b
<VAR>α : Type u_7<VAR>MulZeroOneClass α<VAR>x : α<GOAL>(MonoidWithZeroHom.id α) x = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g : β →*₀ γ<VAR>f : α →*₀ β<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g : β →*₀ γ<VAR>f : α →*₀ β<VAR>x : α<GOAL>(g.comp f) x = g (f x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>MulZeroOneClass δ<VAR>f : α →*₀ β<VAR>g : β →*₀ γ<VAR>h : γ →*₀ δ<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g₁ g₂ : β →*₀ γ<VAR>f : α →*₀ β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>MulZeroOneClass γ<VAR>g : β →*₀ γ<VAR>f₁ f₂ : α →*₀ β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<GOAL>Function.Injective MonoidWithZeroHom.toMonoidHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<GOAL>Function.Injective MonoidWithZeroHom.toZeroHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>f.comp (MonoidWithZeroHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulZeroOneClass α<VAR>MulZeroOneClass β<VAR>f : α →*₀ β<GOAL>(MonoidWithZeroHom.id β).comp f = f
<VAR>M₀ : Type u_6<VAR>CommMonoidWithZero M₀<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⇑(powMonoidWithZeroHom hn) = fun x => x ^ n
<VAR>M₀ : Type u_6<VAR>CommMonoidWithZero M₀<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : M₀<GOAL>(powMonoidWithZeroHom hn) a = a ^ n
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<GOAL>0 ∈ Set.center M₀
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>s : Set M₀<GOAL>0 ∈ s.centralizer
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<GOAL>Set.center G₀ˣ ⊆ Units.val ⁻¹' Set.center G₀
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<GOAL>Set.center G₀ˣ = Units.val ⁻¹' Set.center G₀
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>s : Set G₀<VAR>a : G₀<VAR>ha : a ∈ s.centralizer<GOAL>a⁻¹ ∈ s.centralizer
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<VAR>ha : a ∈ s.centralizer<VAR>hb : b ∈ s.centralizer<GOAL>a / b ∈ s.centralizer
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>ha : a ∈ Set.center G₀<GOAL>a⁻¹ ∈ Set.center G₀
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>ha : a ∈ Set.center G₀<VAR>hb : b ∈ Set.center G₀<GOAL>a / b ∈ Set.center G₀
<VAR>M₀ : Type u_1<VAR>CommMonoidWithZero M₀<GOAL>∀ (a : M₀ × M₀), mulMonoidWithZeroHom a = (↑mulMonoidHom).toFun a
<VAR>M₀ : Type u_1<VAR>CommGroupWithZero M₀<GOAL>∀ (a : M₀ × M₀), divMonoidWithZeroHom a = (↑divMonoidHom).toFun a
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>MulZeroOneClass M₀<VAR>Nontrivial M₀<VAR>Zero M₀'<VAR>One M₀'<VAR>f : M₀' → M₀<VAR>zero : f 0 = 0<VAR>one : f 1 = 1<GOAL>Nontrivial M₀'
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a⁻¹ ≠ 0
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a⁻¹ * a = 1
<VAR>M₀ : Type u<VAR>self : MulZeroClass M₀<VAR>a : M₀<GOAL>0 * a = 0
<VAR>M₀ : Type u<VAR>self : MulZeroClass M₀<VAR>a : M₀<GOAL>a * 0 = 0
<VAR>M₀ : Type u<VAR>Mul M₀<VAR>Zero M₀<VAR>self : IsLeftCancelMulZero M₀<VAR>a b c : M₀<GOAL>a ≠ 0 → a * b = a * c → b = c
<VAR>M₀ : Type u_1<VAR>Mul M₀<VAR>Zero M₀<VAR>IsLeftCancelMulZero M₀<VAR>a b c : M₀<VAR>ha : a ≠ 0<VAR>h : a * b = a * c<GOAL>b = c
<VAR>M₀ : Type u_1<VAR>Mul M₀<VAR>Zero M₀<VAR>IsLeftCancelMulZero M₀<VAR>a : M₀<VAR>ha : a ≠ 0<GOAL>Function.Injective fun x => a * x
<VAR>M₀ : Type u<VAR>Mul M₀<VAR>Zero M₀<VAR>self : IsRightCancelMulZero M₀<VAR>a b c : M₀<GOAL>b ≠ 0 → a * b = c * b → a = c
<VAR>M₀ : Type u_1<VAR>Mul M₀<VAR>Zero M₀<VAR>IsRightCancelMulZero M₀<VAR>a b c : M₀<VAR>hb : b ≠ 0<VAR>h : a * b = c * b<GOAL>a = c
<VAR>M₀ : Type u_1<VAR>Mul M₀<VAR>Zero M₀<VAR>IsRightCancelMulZero M₀<VAR>b : M₀<VAR>hb : b ≠ 0<GOAL>Function.Injective fun a => a * b
<VAR>M₀ : Type u_4<VAR>Mul M₀<VAR>Zero M₀<VAR>self : NoZeroDivisors M₀<VAR>a b : M₀<GOAL>a * b = 0 → a = 0 ∨ b = 0
<VAR>M₀ : Type u_1<VAR>CancelMonoidWithZero M₀<VAR>a b c : M₀<VAR>hc : c ≠ 0<GOAL>a * c = b * c ↔ a = b
<VAR>M₀ : Type u_1<VAR>CancelMonoidWithZero M₀<VAR>a b c : M₀<VAR>ha : a ≠ 0<GOAL>a * b = a * c ↔ b = c
<VAR>M₀ : Type u_1<VAR>CommSemigroup M₀<VAR>Zero M₀<VAR>IsLeftCancelMulZero M₀<GOAL>IsRightCancelMulZero M₀
<VAR>M₀ : Type u_1<VAR>CommSemigroup M₀<VAR>Zero M₀<VAR>IsRightCancelMulZero M₀<GOAL>IsLeftCancelMulZero M₀
<VAR>M₀ : Type u_1<VAR>CommSemigroup M₀<VAR>Zero M₀<VAR>IsLeftCancelMulZero M₀<GOAL>IsCancelMulZero M₀
<VAR>M₀ : Type u_1<VAR>CommSemigroup M₀<VAR>Zero M₀<VAR>IsRightCancelMulZero M₀<GOAL>IsCancelMulZero M₀
<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>Div M₀<VAR>self : MulDivCancelClass M₀<VAR>a b : M₀<GOAL>b ≠ 0 → a * b / b = a
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>Div M₀<VAR>MulDivCancelClass M₀<VAR>b : M₀<VAR>a : M₀<VAR>hb : b ≠ 0<GOAL>a * b / b = a
<VAR>M₀ : Type u_1<VAR>CommMonoidWithZero M₀<VAR>Div M₀<VAR>MulDivCancelClass M₀<VAR>a : M₀<VAR>b : M₀<VAR>ha : a ≠ 0<GOAL>a * b / a = b
<VAR>G₀ : Type u<VAR>self : GroupWithZero G₀<VAR>a : G₀<GOAL>a ≠ 0 → a * a⁻¹ = 1
<VAR>G₀ : Type u<VAR>self : GroupWithZero G₀<GOAL>0⁻¹ = 0
<VAR>G₀ : Type u<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a * a⁻¹ = 1
<VAR>M₀ : Type u_1<VAR>CancelMonoidWithZero M₀<VAR>x : M₀<VAR>hx : x ^ 2 = x<GOAL>x = 0 ∨ x = 1
<VAR>G₀ : Type u<VAR>GroupWithZero G₀<VAR>b : G₀<VAR>h : b ≠ 0<VAR>a : G₀<GOAL>a * b * b⁻¹ = a
<VAR>G₀ : Type u<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<VAR>b : G₀<GOAL>a * (a⁻¹ * b) = b
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>a : M₀<VAR>h : a = 0<VAR>b : M₀<GOAL>a * b = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>a : M₀<VAR>b : M₀<VAR>h : b = 0<GOAL>a * b = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<GOAL>a * b = 0 ↔ a = 0 ∨ b = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<GOAL>0 = a * b ↔ a = 0 ∨ b = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<GOAL>a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<GOAL>a * b = 0 ↔ b * a = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a b : M₀<GOAL>a * b ≠ 0 ↔ b * a ≠ 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a : M₀<GOAL>a * a = 0 ↔ a = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a : M₀<GOAL>0 = a * a ↔ a = 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a : M₀<GOAL>a * a ≠ 0 ↔ a ≠ 0
<VAR>M₀ : Type u_1<VAR>MulZeroClass M₀<VAR>NoZeroDivisors M₀<VAR>a : M₀<GOAL>0 ≠ a * a ↔ a ≠ 0
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_3<VAR>Mul M₀<VAR>Zero M₀<VAR>Mul M₀'<VAR>Zero M₀'<VAR>f : M₀ → M₀'<VAR>hf : Function.Injective f<VAR>zero : f 0 = 0<VAR>mul : ∀ (x y : M₀), f (x * y) = f x * f y<VAR>NoZeroDivisors M₀'<GOAL>NoZeroDivisors M₀
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_3<VAR>Mul M₀<VAR>Zero M₀<VAR>Mul M₀'<VAR>Zero M₀'<VAR>f : M₀ → M₀'<VAR>hf : Function.Injective f<VAR>zero : f 0 = 0<VAR>mul : ∀ (x y : M₀), f (x * y) = f x * f y<VAR>IsLeftCancelMulZero M₀'<GOAL>IsLeftCancelMulZero M₀
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_3<VAR>Mul M₀<VAR>Zero M₀<VAR>Mul M₀'<VAR>Zero M₀'<VAR>f : M₀ → M₀'<VAR>hf : Function.Injective f<VAR>zero : f 0 = 0<VAR>mul : ∀ (x y : M₀), f (x * y) = f x * f y<VAR>IsRightCancelMulZero M₀'<GOAL>IsRightCancelMulZero M₀
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a b : M₀<VAR>h : Commute a b<GOAL>Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
<VAR>M₀ : Type u_8<VAR>CommMonoidWithZero M₀<VAR>a b : M₀<GOAL>Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>r : M₀<VAR>n : ℕ<GOAL>Ring.inverse r ^ n = Ring.inverse (r ^ n)
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>a b : M₀<VAR>h : Commute a b<GOAL>Commute (Ring.inverse a) (Ring.inverse b)
<VAR>G₀ : Type u_3<VAR>MulZeroClass G₀<VAR>a : G₀<GOAL>Commute a 0
<VAR>G₀ : Type u_3<VAR>MulZeroClass G₀<VAR>a : G₀<GOAL>Commute 0 a
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<GOAL>Commute a⁻¹ b ↔ Commute a b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : Commute a b<GOAL>Commute a⁻¹ b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<GOAL>Commute a b⁻¹ ↔ Commute a b
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b : G₀<VAR>h : Commute a b<GOAL>Commute a b⁻¹
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hab : Commute a b<VAR>hac : Commute a c<GOAL>Commute a (b / c)
<VAR>G₀ : Type u_3<VAR>GroupWithZero G₀<VAR>a b c : G₀<VAR>hac : Commute a c<VAR>hbc : Commute b c<GOAL>Commute (a / b) c
<VAR>G₀ : Type u_8<VAR>GroupWithZero G₀<VAR>a : G₀<VAR>m n : ℕ<GOAL>a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
<VAR>α : Type u_1<VAR>One α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : α<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : WithZero α<VAR>hxy : x * y ≠ 0<GOAL>WithZero.unzero hxy = WithZero.unzero ⋯ * WithZero.unzero ⋯
<VAR>α : Type u_1<VAR>MulOneClass α<GOAL>∀ (a : α), WithZero.coeMonoidHom a = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulZeroOneClass β<VAR>f g : WithZero α →*₀ β<VAR>h : (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulZeroOneClass β<VAR>F : WithZero α →*₀ β<GOAL>∀ (a : α), (WithZero.lift'.symm F) a = F ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulZeroOneClass β<VAR>f : α →* β<GOAL>(WithZero.lift' f) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulZeroOneClass β<VAR>f : α →* β<VAR>x : α<GOAL>(WithZero.lift' f) ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulZeroOneClass β<VAR>f : WithZero α →*₀ β<GOAL>f = WithZero.lift' ((↑f).comp WithZero.coeMonoidHom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<GOAL>(WithZero.map' f) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>x : α<GOAL>(WithZero.map' f) ↑x = ↑(f x)
<VAR>β : Type u_2<VAR>MulOneClass β<GOAL>↑(WithZero.map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>f : α →* β<VAR>g : β →* γ<VAR>x : WithZero α<GOAL>(WithZero.map' g) ((WithZero.map' f) x) = (WithZero.map' (g.comp f)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MulOneClass γ<VAR>f : α →* β<VAR>g : β →* γ<GOAL>WithZero.map' (g.comp f) = (WithZero.map' g).comp (WithZero.map' f)
<VAR>α : Type u_1<VAR>One α<VAR>Pow α ℕ<VAR>a : α<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>α : Type u_1<VAR>Inv α<GOAL>0⁻¹ = 0
<VAR>α : Type u_1<VAR>Div α<VAR>a b : α<GOAL>↑(a / b) = ↑a / ↑b
<VAR>α : Type u_1<VAR>One α<VAR>Pow α ℤ<VAR>a : α<VAR>n : ℤ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u<VAR>MulZeroOneClass α<VAR>a : α<VAR>Nontrivial α<VAR>Invertible a<GOAL>a ≠ 0
<VAR>α : Type u<VAR>MonoidWithZero α<VAR>x : α<VAR>Invertible x<GOAL>Ring.inverse x = ⅟x
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a : α<VAR>Invertible a<GOAL>⅟a = a⁻¹
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a : α<VAR>Invertible a<GOAL>a⁻¹ * a = 1
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a : α<VAR>Invertible a<GOAL>a * a⁻¹ = 1
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a b : α<VAR>Invertible b<GOAL>a / b * b = a
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a b : α<VAR>Invertible b<GOAL>a * b / b = a
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a : α<VAR>Invertible a<GOAL>a / a = 1
<VAR>α : Type u<VAR>GroupWithZero α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<VAR>Invertible (a / b)<GOAL>⅟(a / b) = b / a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsNilpotent R L<GOAL>LieAlgebra.rootSpace ⊤ 0 = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>χ : ↥H → R<GOAL>LieSubmodule.comap H.incl' (LieAlgebra.rootSpace H χ) = LieModule.weightSpace (↥H) χ
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ LieAlgebra.rootSpace H χ₁<VAR>hm : m ∈ LieModule.weightSpace M χ₂<GOAL>⁅x, m⁆ ∈ LieModule.weightSpace M (χ₁ + χ₂)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ LieAlgebra.rootSpace H χ₁<VAR>hm : m ∈ LieModule.weightSpace M χ₂<VAR>n : ℕ<GOAL>((LieModule.toEnd R L M) x ^ n) m ∈ LieModule.weightSpace M (n • χ₁ + χ₂)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>χ₁ χ₂ χ₃ : ↥H → R<VAR>hχ : χ₁ + χ₂ = χ₃<VAR>x : ↥(LieAlgebra.rootSpace H χ₁)<VAR>m : ↥(LieModule.weightSpace M χ₂)<GOAL>↑((LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>α χ : ↥H → R<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H α<GOAL>Set.MapsTo ⇑((LieModule.toEnd R L M) x) ↑(LieModule.weightSpace M χ) ↑(LieModule.weightSpace M (α + χ))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<GOAL>LieAlgebra.rootSpaceProduct R L H = LieAlgebra.rootSpaceWeightSpaceProduct R L H L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>χ₁ χ₂ χ₃ : ↥H → R<VAR>hχ : χ₁ + χ₂ = χ₃<VAR>x : ↥(LieAlgebra.rootSpace H χ₁)<VAR>y : ↥(LieAlgebra.rootSpace H χ₂)<GOAL>↑((LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<GOAL>(LieAlgebra.zeroRootSubalgebra R L H).toSubmodule = ↑(LieAlgebra.rootSpace H 0)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>x : L<GOAL>x ∈ LieAlgebra.zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ k, ((LieModule.toEnd R (↥H) L) y ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<GOAL>H.toLieSubmodule ≤ LieAlgebra.rootSpace H 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<GOAL>H ≤ LieAlgebra.zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<GOAL>(LieAlgebra.zeroRootSubalgebra R L H).normalizer = LieAlgebra.zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>h : LieAlgebra.zeroRootSubalgebra R L H = H<GOAL>H.IsCartanSubalgebra
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<GOAL>LieAlgebra.zeroRootSubalgebra R L H = H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>IsNoetherian R L<GOAL>LieAlgebra.zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<GOAL>LieAlgebra.rootSpace H 0 = H.toLieSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<GOAL>x ∈ LieAlgebra.corootSpace α ↔ ↑x ∈ Submodule.span R {x | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = x}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>LieAlgebra.IsNilpotent R ↥H<VAR>H.IsCartanSubalgebra<VAR>IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<GOAL>x ∈ LieAlgebra.corootSpace α ↔ x ∈ Submodule.span R {x | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = ↑x}
<VAR>α : Type u_1<VAR>SemigroupWithZero α<VAR>a : α<VAR>h : 0 ∣ a<GOAL>a = 0
<VAR>α : Type u_1<VAR>SemigroupWithZero α<VAR>a : α<GOAL>0 ∣ a ↔ a = 0
<VAR>α : Type u_1<VAR>SemigroupWithZero α<VAR>a : α<GOAL>a ∣ 0
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>a b c : α<VAR>ha : a ≠ 0<GOAL>a * b ∣ a * c ↔ b ∣ c