ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<GOAL>(↑D).toFun = ⇑D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>f : L →ₗ[R] M<VAR>h₁ : ∀ (a b : L), f ⁅a, b⁆ = ⁅a, f b⁆ - ⁅b, f a⁆<GOAL>⇑{ toLinearMap := f, leibniz' := h₁ } = ⇑f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>f : LieDerivation R L M<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<VAR>H : ∀ (a : L), D1 a = D2 a<GOAL>D1 = D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<VAR>h : D1 = D2<VAR>a : L<GOAL>D1 a = D2 a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<VAR>a b : L<GOAL>D ⁅a, b⁆ = ⁅a, D b⁆ - ⁅b, D a⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D : LieDerivation R L L<VAR>a b : L<GOAL>D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<VAR>s : Set L<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<GOAL>Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<VAR>s : Set L<VAR>hs : LieSubalgebra.lieSpan R L s = ⊤<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<GOAL>D1 = D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>⇑0 = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>↑0 = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>a : L<GOAL>0 a = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<GOAL>⇑(D1 + D2) = ⇑D1 + ⇑D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<GOAL>↑(D1 + D2) = ↑D1 + ↑D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<VAR>a : L<GOAL>(D1 + D2) a = D1 a + D2 a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<VAR>a : L<GOAL>D (-a) = -D a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<VAR>a b : L<GOAL>D (a - b) = D a - D b
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<GOAL>⇑(-D) = -⇑D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<GOAL>↑(-D) = -↑D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<VAR>a : L<GOAL>(-D) a = -D a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<GOAL>⇑(D1 - D2) = ⇑D1 - ⇑D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D1 D2 : LieDerivation R L M<GOAL>↑(D1 - D2) = ↑D1 - ↑D2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>a : L<VAR>D1 D2 : LieDerivation R L M<GOAL>(D1 - D2) a = D1 a - D2 a
<VAR>S : Type u_4<VAR>L : Type u_5<VAR>α : Type u_6<VAR>SMul S α<VAR>LieRing L<VAR>AddCommGroup α<VAR>LieRingModule L α<VAR>self : LieDerivation.SMulBracketCommClass S L α<VAR>s : S<VAR>l : L<VAR>a : α<GOAL>s • ⁅l, a⁆ = ⁅l, s • a⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>S : Type u_4<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>LieDerivation.SMulBracketCommClass S L M<VAR>r : S<VAR>D : LieDerivation R L M<GOAL>⇑(r • D) = r • ⇑D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>S : Type u_4<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>LieDerivation.SMulBracketCommClass S L M<VAR>r : S<VAR>D : LieDerivation R L M<GOAL>↑(r • D) = r • ↑D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>a : L<VAR>S : Type u_4<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>LieDerivation.SMulBracketCommClass S L M<VAR>r : S<VAR>D : LieDerivation R L M<GOAL>(r • D) a = r • D a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D1 D2 : LieDerivation R L L<GOAL>↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D1 D2 : LieDerivation R L L<VAR>a : L<GOAL>⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>D₁ D₂ : LieDerivation R L L<VAR>x : L<GOAL>⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>Function.Injective ⇑(LieDerivation.toLinearMapLieHom R L)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>m : M<GOAL>∀ (m_1 : L), ((LieDerivation.inner R L M) m) m_1 = ⁅m_1, m⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<GOAL>⁅x, D⁆ y = ⁅y, D x⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D : LieDerivation R L M<GOAL>⁅x, ↑D⁆ = ↑⁅x, D⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<VAR>D₁ D₂ : LieDerivation R L L<GOAL>⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a : lib R X<VAR>b c : lib R X<VAR>h : FreeLieAlgebra.Rel R X b c<GOAL>FreeLieAlgebra.Rel R X (a + b) (a + c)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a b : lib R X<VAR>h : FreeLieAlgebra.Rel R X a b<GOAL>FreeLieAlgebra.Rel R X (-a) (-b)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a : lib R X<VAR>b c : lib R X<VAR>h : FreeLieAlgebra.Rel R X b c<GOAL>FreeLieAlgebra.Rel R X (a - b) (a - c)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a b : lib R X<VAR>c : lib R X<VAR>h : FreeLieAlgebra.Rel R X a b<GOAL>FreeLieAlgebra.Rel R X (a - c) (b - c)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>S : Type u_1<VAR>Monoid S<VAR>DistribMulAction S R<VAR>IsScalarTower S R R<VAR>t : S<VAR>a b : lib R X<VAR>h : FreeLieAlgebra.Rel R X a b<GOAL>FreeLieAlgebra.Rel R X (t • a) (t • b)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>t : R<VAR>a : lib R X<GOAL>(FreeLieAlgebra.liftAux R f) (t • a) = t • (FreeLieAlgebra.liftAux R f) a
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>a b : lib R X<GOAL>(FreeLieAlgebra.liftAux R f) (a + b) = (FreeLieAlgebra.liftAux R f) a + (FreeLieAlgebra.liftAux R f) b
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>a b : lib R X<GOAL>(FreeLieAlgebra.liftAux R f) (a * b) = ⁅(FreeLieAlgebra.liftAux R f) a, (FreeLieAlgebra.liftAux R f) b⁆
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>a b : lib R X<VAR>h : FreeLieAlgebra.Rel R X a b<GOAL>(FreeLieAlgebra.liftAux R f) a = (FreeLieAlgebra.liftAux R f) b
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>F : FreeLieAlgebra R X →ₗ⁅R⁆ L<GOAL>(FreeLieAlgebra.lift R).symm F = ⇑F ∘ FreeLieAlgebra.of R
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<GOAL>⇑((FreeLieAlgebra.lift R) f) ∘ FreeLieAlgebra.of R = f
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>g : FreeLieAlgebra R X →ₗ⁅R⁆ L<GOAL>⇑g ∘ FreeLieAlgebra.of R = f ↔ g = (FreeLieAlgebra.lift R) f
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>f : X → L<VAR>x : X<GOAL>((FreeLieAlgebra.lift R) f) (FreeLieAlgebra.of R x) = f x
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>F : FreeLieAlgebra R X →ₗ⁅R⁆ L<GOAL>(FreeLieAlgebra.lift R) (⇑F ∘ FreeLieAlgebra.of R) = F
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>L : Type w<VAR>LieRing L<VAR>LieAlgebra R L<VAR>F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L<VAR>h : ∀ (x : X), F₁ (FreeLieAlgebra.of R x) = F₂ (FreeLieAlgebra.of R x)<GOAL>F₁ = F₂
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a : UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)<GOAL>(FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X) a = ((UniversalEnvelopingAlgebra.lift R) ((FreeLieAlgebra.lift R) (FreeAlgebra.ι R))) a
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>a : FreeAlgebra R X<GOAL>(FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X).symm a = ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ FreeLieAlgebra.of R)) a
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>x : L<VAR>m : M<VAR>n : N<GOAL>⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>AddCommGroup P<VAR>Module R P<VAR>LieRingModule L P<VAR>LieModule R L P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.LieModule.lift R L M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>AddCommGroup P<VAR>Module R P<VAR>LieRingModule L P<VAR>LieModule R L P<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<GOAL>⇑((TensorProduct.LieModule.liftLie R L M N P) f) = ⇑((TensorProduct.LieModule.lift R L M N P) ↑f)
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>AddCommGroup P<VAR>Module R P<VAR>LieRingModule L P<VAR>LieModule R L P<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.LieModule.liftLie R L M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>AddCommGroup P<VAR>Module R P<VAR>LieRingModule L P<VAR>LieModule R L P<VAR>AddCommGroup Q<VAR>Module R Q<VAR>LieRingModule L Q<VAR>LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ P<VAR>g : N →ₗ⁅R,L⁆ Q<GOAL>↑(TensorProduct.LieModule.map f g) = TensorProduct.map ↑f ↑g
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>AddCommGroup P<VAR>Module R P<VAR>LieRingModule L P<VAR>LieModule R L P<VAR>AddCommGroup Q<VAR>Module R Q<VAR>LieRingModule L Q<VAR>LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ P<VAR>g : N →ₗ⁅R,L⁆ Q<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.LieModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<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 N<VAR>Module R N<VAR>LieRingModule L N<VAR>LieModule R L N<VAR>M' : LieSubmodule R L M<VAR>N' : LieSubmodule R L N<GOAL>TensorProduct.LieModule.mapIncl M' N' = TensorProduct.LieModule.map M'.incl N'.incl
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<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<GOAL>(LieModule.toModuleHom R L M) (x ⊗ₜ[R] m) = ⁅x, m⁆
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>LieRing L<VAR>LieAlgebra R L<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<GOAL>⁅I, N⁆ = ((LieModule.toModuleHom R L M).comp (TensorProduct.LieModule.mapIncl I N)).range
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>m : M<GOAL>m ∈ N.normalizer ↔ ∀ (x : L), ⁅x, m⁆ ∈ N
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>N ≤ N.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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<GOAL>(N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>h : N₁ ≤ N₂<GOAL>N₁.normalizer ≤ N₂.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Monotone LieSubmodule.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : 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>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>LieModule R L M'<VAR>N : LieSubmodule R L M<VAR>f : M' →ₗ⁅R,L⁆ M<GOAL>LieSubmodule.comap f N.normalizer = (LieSubmodule.comap f N).normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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<GOAL>⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>GaloisConnection (fun N => ⁅⊤, N⁆) LieSubmodule.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>⊥.normalizer = LieModule.maxTrivSubmodule R L M
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>x ∈ N.idealizer ↔ ∀ (m : M), ⁅x, m⁆ ∈ N
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>LieSubmodule.idealizer I = LieSubmodule.normalizer I
<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>x : L<GOAL>x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ 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>x : L<GOAL>x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ 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<GOAL>H ≤ H.normalizer
<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<GOAL>↑H.toLieSubmodule.normalizer = H.normalizer.toSubmodule
<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>x y z : L<VAR>hx : x ∈ H.normalizer<VAR>hy : y ∈ Submodule.span R {x} ⊔ H.toSubmodule<VAR>hz : z ∈ Submodule.span R {x} ⊔ H.toSubmodule<GOAL>⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
<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>x y : L<VAR>hx : x ∈ H.normalizer<VAR>hy : y ∈ H<GOAL>⁅x, y⁆ ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H K : LieSubalgebra R L<VAR>h₁ : H ≤ K<VAR>h₂ : K ≤ H.normalizer<GOAL>∃ I, lieIdealSubalgebra R (↥K) I = LieSubalgebra.ofLe 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<GOAL>H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥
<VAR>R : Type u<VAR>self : EuclideanDomain R<VAR>a : R<GOAL>EuclideanDomain.quotient a 0 = 0
<VAR>R : Type u<VAR>self : EuclideanDomain R<VAR>a b : R<GOAL>b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a
<VAR>R : Type u<VAR>self : EuclideanDomain R<GOAL>WellFounded EuclideanDomain.r
<VAR>R : Type u<VAR>self : EuclideanDomain R<VAR>a : R<VAR>b : R<GOAL>b ≠ 0 → ¬EuclideanDomain.r (a * b) a
<VAR>R : Type u<VAR>self : EuclideanDomain R<VAR>a : R<VAR>b : R<GOAL>b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b : R<GOAL>b * (a / b) + a % b = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b : R<GOAL>a % b + b * (a / b) = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>m k : R<GOAL>m % k + m / k * k = m
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>m k : R<GOAL>m / k * k + m % k = m
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>a b : R<GOAL>a % b = a - b * (a / b)
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<VAR>b : R<GOAL>b ≠ 0 → EuclideanDomain.r (a % b) b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<VAR>b : R<VAR>h : a ≠ 0<GOAL>¬EuclideanDomain.r (a * b) b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>a % 0 = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>EuclideanDomain.r a 1 → a = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b : R<GOAL>b ∣ a → a ≠ 0 → ¬EuclideanDomain.r a b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>a / 0 = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>P : R → R → Prop<VAR>a b : R<VAR>H0 : ∀ (x : R), P 0 x<VAR>H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b<GOAL>P a b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a : R<GOAL>EuclideanDomain.gcd 0 a = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>s t r' s' t' : R<GOAL>EuclideanDomain.xgcdAux 0 s t r' s' t' = (r', s', t')
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>r s t r' s' t' : R<VAR>h : r ≠ 0<GOAL>EuclideanDomain.xgcdAux r s t r' s' t' = EuclideanDomain.xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>s : R<GOAL>EuclideanDomain.gcdA 0 s = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>s : R<GOAL>EuclideanDomain.gcdB 0 s = 1
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>x y : R<GOAL>EuclideanDomain.xgcd x y = (EuclideanDomain.gcdA x y, EuclideanDomain.gcdB x y)
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b : R<GOAL>a % b = 0 ↔ b ∣ a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>a % a = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c : R<VAR>h : c ∣ b<GOAL>c ∣ a % b ↔ c ∣ a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>a % 1 = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>b : R<GOAL>0 % b = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<GOAL>0 / a = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>a / a = 1
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c : R<VAR>hb : b ≠ 0<VAR>h : a * b = c<GOAL>a = c / b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>h : a * b = c<GOAL>b = c / a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>x : R<VAR>y z : R<VAR>h : z ∣ y<GOAL>x * y / z = x * (y / z)
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b : R<VAR>hb : b ≠ 0<VAR>hab : b ∣ a<GOAL>b * (a / b) = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>p : R<GOAL>p / 1 = p
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>p q : R<VAR>hpq : q ∣ p<GOAL>p / q ∣ p
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>a b c : R<VAR>h : a * b ∣ c<GOAL>b ∣ c / a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a : R<GOAL>EuclideanDomain.gcd a 0 = a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b = EuclideanDomain.gcd (b % a) a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b ∣ a
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b ∣ b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b = 0 ↔ a = 0 ∧ b = 0
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b c : R<GOAL>c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>DecidableEq R<VAR>a b : R<GOAL>EuclideanDomain.gcd a b = a ↔ a ∣ b