ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>K : Type u_3<VAR>VAdd K H<VAR>VAddAssocClass K H H<VAR>c : K<VAR>f : AddConstMap G H a b<GOAL>⇑(c +ᵥ f) = c +ᵥ ⇑f
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>f g : AddConstMap G G a a<GOAL>f * g = f.comp g
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>f g : AddConstMap G G a a<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>1 = AddConstMap.id
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>⇑1 = id
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>f : AddConstMap G G a a<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>f : AddConstMap G G a a<VAR>n : ℕ<VAR>x : G<GOAL>(f ^ n) x = (⇑f)^[n] x
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>⇑AddConstMap.toEnd = DFunLike.coe
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>K : Type u_3<VAR>Add G<VAR>AddZeroClass H<VAR>a : G<VAR>b : H<VAR>DistribSMul K H<VAR>c : K<VAR>f : AddConstMap G H a b<GOAL>⇑(AddConstMap.smul c f) = c • ⇑f
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>a : G<VAR>c : Multiplicative G<GOAL>⇑(AddConstMap.addLeftHom c) = c • id
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<VAR>x : G<GOAL>(AddConstMap.conjNeg f) x = -f (-x)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>a : G<VAR>b : H<GOAL>AddConstMap.conjNeg.symm = AddConstMap.conjNeg
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>p : AddSubmonoid M<VAR>hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p<VAR>hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p<GOAL>↑(Subbimodule.mk p hA hB) = ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a • m ∈ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>b : B<VAR>m : M<VAR>hm : m ∈ p<GOAL>b • m ∈ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Module S M<VAR>Algebra S A<VAR>Algebra S B<VAR>IsScalarTower S A M<VAR>IsScalarTower S B M<VAR>p : Submodule (A ⊗[R] B) M<GOAL>↑(Subbimodule.baseChange S p) = ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<GOAL>↑(Subbimodule.toSubmodule p) = ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<GOAL>↑(Subbimodule.toSubmodule' p) = ↑p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>p : Submodule (R ⊗[ℕ] S) M<GOAL>↑(Subbimodule.toSubbimoduleInt R S M p) = ↑p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>p : Submodule (R ⊗[ℤ] S) M<GOAL>↑(Subbimodule.toSubbimoduleNat R S M p) = ↑p
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>(i : ι) → VAdd K (R i)<VAR>r : K<VAR>s : Set ι<VAR>t : (i : ι) → Set (R i)<GOAL>r +ᵥ s.pi t ⊆ s.pi (r +ᵥ t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>(i : ι) → SMul K (R i)<VAR>r : K<VAR>s : Set ι<VAR>t : (i : ι) → Set (R i)<GOAL>r • s.pi t ⊆ s.pi (r • t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>(i : ι) → SMul K (R i)<VAR>r : K<VAR>t : (i : ι) → Set (R i)<GOAL>r • Set.univ.pi t = Set.univ.pi (r • t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>(i : ι) → VAdd K (R i)<VAR>r : K<VAR>t : (i : ι) → Set (R i)<GOAL>r +ᵥ Set.univ.pi t = Set.univ.pi (r +ᵥ t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>Group K<VAR>(i : ι) → MulAction K (R i)<VAR>r : K<VAR>S : Set ι<VAR>t : (i : ι) → Set (R i)<GOAL>r • S.pi t = S.pi (r • t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>AddGroup K<VAR>(i : ι) → AddAction K (R i)<VAR>r : K<VAR>S : Set ι<VAR>t : (i : ι) → Set (R i)<GOAL>r +ᵥ S.pi t = S.pi (r +ᵥ t)
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>GroupWithZero K<VAR>(i : ι) → MulAction K (R i)<VAR>r : K<VAR>S : Set ι<VAR>t : (i : ι) → Set (R i)<VAR>hr : r ≠ 0<GOAL>r • S.pi t = S.pi (r • t)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>hM : Module.IsTorsionBySet R M ↑I<GOAL>DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDedekindDomain R<VAR>Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDedekindDomain R<VAR>Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ e p)
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>F : Type u_3<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_4<VAR>S : Type u_5<VAR>DivisionRing R<VAR>DivisionRing S<VAR>Module R M<VAR>Module S M₂<VAR>c : ℚ<VAR>x : M<GOAL>f (↑c • x) = ↑c • f x
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>_instM : Module ℚ M<VAR>_instM₂ : Module ℚ M₂<VAR>F : Type u_3<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>c : ℚ<VAR>x : M<GOAL>f (c • x) = c • f x
<VAR>E : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>AddCommGroup E<VAR>DivisionRing R<VAR>DivisionRing S<VAR>Module R E<VAR>Module S E<VAR>r : ℚ<VAR>x : E<GOAL>↑r • x = ↑r • x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>1 = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : Module.End R M<GOAL>f * g = f ∘ₗ g
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>1 x = x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : Module.End R M<VAR>x : M<GOAL>(f * g) x = f (g x)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑1 = id
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : Module.End R M<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>m : M<GOAL>↑n m = n • m
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>m : M<GOAL>(OfNat.ofNat n) m = OfNat.ofNat n • m
<VAR>R : Type u_1<VAR>N₁ : Type u_10<VAR>Semiring R<VAR>AddCommGroup N₁<VAR>Module R N₁<VAR>z : ℤ<VAR>m : N₁<GOAL>↑z m = z • m
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<VAR>h : IsUnit f<VAR>x : M<GOAL>f (h.unit.inv x) = x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<VAR>h : IsUnit f<VAR>x : M<GOAL>h.unit.inv (f x) = x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>m : M<GOAL>(f ^ n) m = (⇑f)^[n] m
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<VAR>m : M<VAR>k l : ℕ<VAR>hk : k ≤ l<VAR>hm : (f ^ k) m = 0<GOAL>(f ^ l) m = 0
<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>f : M →ₛₗ[σ₁₂] M₂<VAR>g : Module.End R M<VAR>g₂ : Module.End R₂ M₂<VAR>h : LinearMap.comp g₂ f = f.comp g<VAR>k : ℕ<GOAL>LinearMap.comp (g₂ ^ k) f = f.comp (g ^ k)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<GOAL>LinearMap.id ^ n = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<GOAL>f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>h : Function.Surjective ⇑f'<VAR>n : ℕ<GOAL>Function.Surjective ⇑(f' ^ n)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>h : Function.Injective ⇑f'<VAR>n : ℕ<GOAL>Function.Injective ⇑(f' ^ n)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>h : Function.Bijective ⇑f'<VAR>n : ℕ<GOAL>Function.Bijective ⇑(f' ^ n)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Function.Injective ⇑(f' ^ n)<GOAL>Function.Injective ⇑f'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Function.Surjective ⇑(f' ^ n)<GOAL>Function.Surjective ⇑f'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<VAR>a : M<GOAL>f • a = f a
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>∀ (a : M), (DistribMulAction.toLinearMap R M s) a = s • a
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>(DistribMulAction.toModuleEnd R M) s = DistribMulAction.toLinearMap R M s
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>(Module.toModuleEnd R M) s = DistribMulAction.toLinearMap R M s
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Module.End R R<GOAL>(Module.moduleEndSelf R).symm f = MulOpposite.op (f 1)
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Rᵐᵒᵖ<GOAL>(Module.moduleEndSelf R) s = DistribMulAction.toLinearMap R R s
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Module.End Rᵐᵒᵖ R<GOAL>(Module.moduleEndSelfOp R).symm f = f 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : R<GOAL>(Module.moduleEndSelfOp R) s = DistribMulAction.toLinearMap Rᵐᵒᵖ R s
<VAR>R : Type u_1<VAR>N₁ : Type u_10<VAR>Semiring R<VAR>n : ℕ<VAR>AddCommMonoid N₁<VAR>Module R N₁<GOAL>↑n = (Module.toModuleEnd R N₁) n
<VAR>R : Type u_1<VAR>N₁ : Type u_10<VAR>Semiring R<VAR>z : ℤ<VAR>AddCommGroup N₁<VAR>Module R N₁<GOAL>↑z = (Module.toModuleEnd R N₁) z
<VAR>R : Type u_1<VAR>S : Type u_4<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>Semiring S<VAR>Module R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<GOAL>⇑(f.smulRight x) = fun c => f c • x
<VAR>R : Type u_1<VAR>S : Type u_4<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>Semiring S<VAR>Module R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>c : M₁<GOAL>(f.smulRight x) c = f c • x
<VAR>R : Type u_1<VAR>S : Type u_4<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>Semiring S<VAR>Module R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<GOAL>f.smulRight 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_4<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>Semiring S<VAR>Module R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>x : M<GOAL>LinearMap.smulRight 0 x = 0
<VAR>R : Type u_1<VAR>S : Type u_4<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>Semiring S<VAR>Module R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>NoZeroSMulDivisors S M<GOAL>f.smulRight x = 0 ↔ f = 0 ∨ x = 0
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M₂<VAR>SMulCommClass R S M₂<VAR>v : M<VAR>f : M →ₗ[R] M₂<GOAL>((LinearMap.applyₗ' S) v) f = f v
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M₂ →ₗ[R] M₃<VAR>g : M →ₗ[R] M₂<GOAL>f.compRight g = f ∘ₗ g
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>v : M<VAR>f : M →ₗ[R] M₂<GOAL>(LinearMap.applyₗ v) f = f v
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M₂ →ₗ[R] R<VAR>x : M<VAR>c : M₂<GOAL>((LinearMap.smulRightₗ f) x) c = f c • x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>x : M<VAR>f g : F<GOAL>x ∈ LinearMap.eqLocus f g ↔ f x = g x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<GOAL>(LinearMap.eqLocus f g).toAddSubmonoid = (↑f).eqLocusM ↑g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<GOAL>LinearMap.eqLocus f g = ⊤ ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>LinearMap.eqLocus f f = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<VAR>S : Submodule R M<GOAL>S ≤ LinearMap.eqLocus f g ↔ Set.EqOn ⇑f ⇑g ↑S
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<VAR>S T : Submodule R M<VAR>hS : Set.EqOn ⇑f ⇑g ↑S<VAR>hT : Set.EqOn ⇑f ⇑g ↑T<GOAL>Set.EqOn ⇑f ⇑g ↑(S ⊔ T)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<VAR>S T : Submodule R M<VAR>hST : Codisjoint S T<VAR>hS : Set.EqOn ⇑f ⇑g ↑S<VAR>hT : Set.EqOn ⇑f ⇑g ↑T<GOAL>f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f g : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.eqLocus f g = LinearMap.ker (f - g)
<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>self : LieSubmodule R L M<VAR>x : L<VAR>m : M<GOAL>m ∈ (↑self).carrier → ⁅x, m⁆ ∈ (↑self).carrier
<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 : LieSubmodule R L M<GOAL>↑↑N = ↑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 : LieSubmodule R L M<VAR>x : M<GOAL>x ∈ (↑N).carrier ↔ x ∈ ↑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>S : Set M<VAR>h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S<VAR>h₂ : S 0<VAR>h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier<VAR>h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier<VAR>x : M<GOAL>x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } ↔ x ∈ S
<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>p : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier<VAR>x : M<GOAL>x ∈ { toSubmodule := p, lie_mem := h } ↔ x ∈ p
<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 : LieSubmodule R L M<VAR>x : M<GOAL>x ∈ ↑N ↔ x ∈ 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 : LieSubmodule R L M<GOAL>0 ∈ 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 : LieSubmodule R L M<VAR>x : M<VAR>h : x ∈ N<GOAL>⟨x, h⟩ = 0 ↔ x = 0
<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>S : Set M<VAR>h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S<VAR>h₂ : S 0<VAR>h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier<VAR>h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier<GOAL>↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } = S
<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>p : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier<GOAL>↑{ toSubmodule := p, lie_mem := h } = p
<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<GOAL>Function.Injective LieSubmodule.toSubmodule
<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<VAR>h : ∀ (m : M), m ∈ N ↔ m ∈ N'<GOAL>N = 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>↑N = ↑N' ↔ N = 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>S : LieSubmodule R L M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<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>S : LieSubmodule R L M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<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 : LieSubmodule R L M<GOAL>↑0 = 0
<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 : LieSubmodule R L M<VAR>m m' : ↥N<GOAL>↑(m + m') = ↑m + ↑m'
<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 : LieSubmodule R L M<VAR>m : ↥N<GOAL>↑(-m) = -↑m
<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 : LieSubmodule R L M<VAR>m m' : ↥N<GOAL>↑(m - m') = ↑m - ↑m'
<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 : LieSubmodule R L M<VAR>t : R<VAR>m : ↥N<GOAL>↑(t • m) = t • ↑m
<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 : LieSubmodule R L M<VAR>x : L<VAR>m : ↥N<GOAL>↑⁅x, m⁆ = ⁅x, ↑m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x y : L<VAR>h : y ∈ I<GOAL>⁅x, y⁆ ∈ 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>x y : L<VAR>h : x ∈ I<GOAL>⁅x, y⁆ ∈ I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>↑(lieIdealSubalgebra R L 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<GOAL>(lieIdealSubalgebra R L I).toSubmodule = ↑I
<VAR>M : Type w<VAR>AddCommGroup M<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<VAR>LieRingModule L M<VAR>x : ↥I<VAR>m : M<GOAL>⁅x, m⁆ = ⁅↑x, m⁆
<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>p : Submodule R M<GOAL>(∃ N, ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<GOAL>↑K.toLieSubmodule = K.toSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ K.toLieSubmodule ↔ x ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<GOAL>(∃ I, lieIdealSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>(∃ I, lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
<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<GOAL>Function.Injective SetLike.coe