ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₄<VAR>AddCommMonoid M₄<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>R₄ : Type u_9<VAR>Semiring R₄<VAR>Module R₄ M₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>h : M₃ →SL[σ₃₄] M₄<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f g : M₁ →L[R₁] M₁<GOAL>f * g = f.comp g
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f g : M₁ →L[R₁] M₁<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f g : M₁ →L[R₁] M₁<VAR>x : M₁<GOAL>(f * g) x = f (g x)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f : M₁ →L[R₁] M₁<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>ContinuousAdd M₁<VAR>self : M₁ →L[R₁] M₁<GOAL>ContinuousLinearMap.toLinearMapRingHom self = ↑self
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>ContinuousAdd M₁<VAR>n : ℕ<VAR>m : M₁<GOAL>↑n m = n • m
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>ContinuousAdd M₁<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>m : M₁<GOAL>(OfNat.ofNat n) m = OfNat.ofNat n • m
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>ContinuousAdd M₁<VAR>f : M₁ →L[R₁] M₁<VAR>a : M₁<GOAL>f • a = f a
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>f₁ : M₁ →L[R₁] M₂<VAR>f₂ : M₁ →L[R₁] M₃<GOAL>↑(f₁.prod f₂) = (↑f₁).prod ↑f₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>f₁ : M₁ →L[R₁] M₂<VAR>f₂ : M₁ →L[R₁] M₃<VAR>x : M₁<GOAL>(f₁.prod f₂) x = (f₁ x, f₂ x)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>x : M₁<GOAL>(ContinuousLinearMap.inl R₁ M₁ M₂) x = (x, 0)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>x : M₂<GOAL>(ContinuousLinearMap.inr R₁ M₁ M₂) x = (0, x)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>↑(ContinuousLinearMap.inl R₁ M₁ M₂) = LinearMap.inl R₁ M₁ M₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>↑(ContinuousLinearMap.inr R₁ M₁ M₂) = LinearMap.inr R₁ M₁ M₂
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>F : Type u_9<VAR>T1Space M₂<VAR>FunLike F M₁ M₂<VAR>ContinuousSemilinearMapClass F σ₁₂ M₁ M₂<VAR>f : F<GOAL>IsClosed ↑(LinearMap.ker f)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_9<VAR>M' : Type u_10<VAR>UniformSpace M'<VAR>CompleteSpace M'<VAR>AddCommMonoid M'<VAR>Module R₁ M'<VAR>T1Space M₂<VAR>FunLike F M' M₂<VAR>ContinuousSemilinearMapClass F σ₁₂ M' M₂<VAR>f : F<GOAL>IsComplete ↑(LinearMap.ker f)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>f : M₁ →L[R₁] M₂<VAR>g : M₁ →L[R₁] M₃<GOAL>LinearMap.ker (f.prod g) = LinearMap.ker f ⊓ LinearMap.ker g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>p : Submodule R₂ M₂<VAR>h : ∀ (x : M₁), f x ∈ p<GOAL>↑(f.codRestrict p h) = LinearMap.codRestrict p (↑f) h
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>p : Submodule R₂ M₂<VAR>h : ∀ (x : M₁), f x ∈ p<VAR>x : M₁<GOAL>↑((f.codRestrict p h) x) = f x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>p : Submodule R₂ M₂<VAR>h : ∀ (x : M₁), f x ∈ p<GOAL>LinearMap.ker (f.codRestrict p h) = LinearMap.ker f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>RingHomSurjective σ₁₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>↑f.rangeRestrict = (↑f).rangeRestrict
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>p : Submodule R₁ M₁<GOAL>↑p.subtypeL = p.subtype
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>p : Submodule R₁ M₁<GOAL>⇑p.subtypeL = ⇑p.subtype
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>p : Submodule R₁ M₁<VAR>x : ↥p<GOAL>p.subtypeL x = ↑x
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>p : Submodule R₁ M₁<GOAL>LinearMap.range p.subtypeL = p
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>p : Submodule R₁ M₁<GOAL>LinearMap.ker p.subtypeL = ⊥
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>↑(ContinuousLinearMap.fst R₁ M₁ M₂) = LinearMap.fst R₁ M₁ M₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>⇑(ContinuousLinearMap.fst R₁ M₁ M₂) = Prod.fst
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>↑(ContinuousLinearMap.snd R₁ M₁ M₂) = LinearMap.snd R₁ M₁ M₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>⇑(ContinuousLinearMap.snd R₁ M₁ M₂) = Prod.snd
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<GOAL>(ContinuousLinearMap.fst R₁ M₁ M₂).prod (ContinuousLinearMap.snd R₁ M₁ M₂) = ContinuousLinearMap.id R₁ (M₁ × M₂)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>f : M₁ →L[R₁] M₂<VAR>g : M₁ →L[R₁] M₃<GOAL>(ContinuousLinearMap.fst R₁ M₂ M₃).comp (f.prod g) = f
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>f : M₁ →L[R₁] M₂<VAR>g : M₁ →L[R₁] M₃<GOAL>(ContinuousLinearMap.snd R₁ M₂ M₃).comp (f.prod g) = g
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₄<VAR>AddCommMonoid M₄<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>Module R₁ M₄<VAR>f₁ : M₁ →L[R₁] M₂<VAR>f₂ : M₃ →L[R₁] M₄<GOAL>↑(f₁.prodMap f₂) = (↑f₁).prodMap ↑f₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₄<VAR>AddCommMonoid M₄<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>Module R₁ M₄<VAR>f₁ : M₁ →L[R₁] M₂<VAR>f₂ : M₃ →L[R₁] M₄<GOAL>⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>ContinuousAdd M₃<VAR>f₁ : M₁ →L[R₁] M₃<VAR>f₂ : M₂ →L[R₁] M₃<GOAL>↑(f₁.coprod f₂) = (↑f₁).coprod ↑f₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>ContinuousAdd M₃<VAR>f₁ : M₁ →L[R₁] M₃<VAR>f₂ : M₂ →L[R₁] M₃<VAR>x : M₁ × M₂<GOAL>(f₁.coprod f₂) x = f₁ x.1 + f₂ x.2
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>ContinuousAdd M₃<VAR>f₁ : M₁ →L[R₁] M₃<VAR>f₂ : M₂ →L[R₁] M₃<GOAL>LinearMap.range (f₁.coprod f₂) = LinearMap.range f₁ ⊔ LinearMap.range f₂
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>Module R₁ M₃<VAR>ContinuousAdd M₃<VAR>f : M₁ →L[R₁] M₃<VAR>g : M₂ →L[R₁] M₃<GOAL>f.comp (ContinuousLinearMap.fst R₁ M₁ M₂) + g.comp (ContinuousLinearMap.snd R₁ M₁ M₂) = f.coprod g
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>TopologicalSpace M'₁<VAR>AddCommMonoid M'₁<VAR>Module R₁ M₁<VAR>Module R₁ M'₁<VAR>ContinuousAdd M₁<VAR>ContinuousAdd M'₁<GOAL>(ContinuousLinearMap.inl R₁ M₁ M'₁).coprod (ContinuousLinearMap.inr R₁ M₁ M'₁) = ContinuousLinearMap.id R₁ (M₁ × M'₁)
<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>R : Type u_10<VAR>S : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R S<VAR>Module S M₂<VAR>IsScalarTower R S M₂<VAR>TopologicalSpace S<VAR>ContinuousSMul S M₂<VAR>c : M₁ →L[R] S<VAR>f : M₂<VAR>x : M₁<GOAL>(c.smulRight f) x = c x • f
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₂<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₂<VAR>c : R₁ →L[R₁] M₂<GOAL>ContinuousLinearMap.smulRight 1 (c 1) = c
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₂<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₂<VAR>f f' : M₂<GOAL>ContinuousLinearMap.smulRight 1 f = ContinuousLinearMap.smulRight 1 f' ↔ f = f'
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₂<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₂<VAR>ContinuousMul R₁<VAR>x : M₂<VAR>c : R₁<GOAL>(ContinuousLinearMap.smulRight 1 x).comp (ContinuousLinearMap.smulRight 1 c) = ContinuousLinearMap.smulRight 1 (c • x)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₁<VAR>x : M₁<VAR>r : R₁<GOAL>(ContinuousLinearMap.toSpanSingleton R₁ x) r = r • x
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₁<VAR>ContinuousAdd M₁<VAR>x y : M₁<GOAL>ContinuousLinearMap.toSpanSingleton R₁ (x + y) = ContinuousLinearMap.toSpanSingleton R₁ x + ContinuousLinearMap.toSpanSingleton R₁ y
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>TopologicalSpace R₁<VAR>ContinuousSMul R₁ M₁<VAR>α : Type u_10<VAR>Monoid α<VAR>DistribMulAction α M₁<VAR>ContinuousConstSMul α M₁<VAR>SMulCommClass R₁ α M₁<VAR>c : α<VAR>x : M₁<GOAL>ContinuousLinearMap.toSpanSingleton R₁ (c • x) = c • ContinuousLinearMap.toSpanSingleton R₁ x
<VAR>R : Type u_10<VAR>M₁ : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>TopologicalSpace R<VAR>TopologicalSpace M₁<VAR>ContinuousSMul R M₁<VAR>c : R<VAR>x : M₁<GOAL>ContinuousLinearMap.toSpanSingleton R (c • x) = c • ContinuousLinearMap.toSpanSingleton R x
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<GOAL>⇑(ContinuousLinearMap.pi f) = fun c i => (f i) c
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<GOAL>↑(ContinuousLinearMap.pi f) = LinearMap.pi fun i => ↑(f i)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<VAR>c : M<VAR>i : ι<GOAL>(ContinuousLinearMap.pi f) c i = (f i) c
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<GOAL>ContinuousLinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<GOAL>(ContinuousLinearMap.pi fun x => 0) = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<VAR>g : M₂ →L[R] M<GOAL>(ContinuousLinearMap.pi f).comp g = ContinuousLinearMap.pi fun i => (f i).comp g
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>i : ι<VAR>b : (i : ι) → φ i<GOAL>(ContinuousLinearMap.proj i) b = b i
<VAR>R : Type u_1<VAR>Semiring R<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →L[R] φ i<VAR>i : ι<GOAL>(ContinuousLinearMap.proj i).comp (ContinuousLinearMap.pi f) = f i
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<GOAL>⨅ i, LinearMap.ker (ContinuousLinearMap.proj i) = ⊥
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (φ i)<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>α : Type u_6<VAR>f : α → ι<VAR>v : (i : ι) → φ i<VAR>i : α<GOAL>(Pi.compRightL R φ f) v i = v (f i)
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>f : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>f (-x) = -f x
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>f : M →SL[σ₁₂] M₂<VAR>x y : M<GOAL>f (x - y) = f x - f y
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>f g : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>(↑f - ↑g) x = f x - g x
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →L[R] M₂<VAR>g : M →L[R] M₃<VAR>h : LinearMap.ker f ⊔ LinearMap.ker g = ⊤<GOAL>LinearMap.range (f.prod g) = (LinearMap.range f).prod (LinearMap.range g)
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>ContinuousAdd M₃<VAR>f : M →L[R] M₃<VAR>g : M₂ →L[R] M₃<GOAL>(LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g)
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>ContinuousAdd M₃<VAR>f : M →L[R] M₃<VAR>g : M₂ →L[R] M₃<VAR>hd : Disjoint (LinearMap.range f) (LinearMap.range g)<GOAL>LinearMap.ker (f.coprod g) = (LinearMap.ker f).prod (LinearMap.ker g)
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>(-f) x = -f x
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f : M →SL[σ₁₂] M₂<GOAL>↑(-f) = -↑f
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f : M →SL[σ₁₂] M₂<GOAL>⇑(-f) = -⇑f
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f g : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>(f - g) x = f x - g x
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f g : M →SL[σ₁₂] M₂<GOAL>↑(f - g) = ↑f - ↑g
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>TopologicalAddGroup M₂<VAR>f g : M →SL[σ₁₂] M₂<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>R₃ : Type u_3<VAR>Ring R₃<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>TopologicalAddGroup M₂<VAR>TopologicalAddGroup M₃<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f : M →SL[σ₁₂] M₂<GOAL>g.comp (-f) = -g.comp f
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>R₃ : Type u_3<VAR>Ring R₃<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>TopologicalAddGroup M₃<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f : M →SL[σ₁₂] M₂<GOAL>(-g).comp f = -g.comp f
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>R₃ : Type u_3<VAR>Ring R₃<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>TopologicalAddGroup M₂<VAR>TopologicalAddGroup M₃<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f₁ f₂ : M →SL[σ₁₂] M₂<GOAL>g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>R₃ : Type u_3<VAR>Ring R₃<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_5<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>TopologicalAddGroup M₃<VAR>g₁ g₂ : M₂ →SL[σ₂₃] M₃<VAR>f : M →SL[σ₁₂] M₂<GOAL>(g₁ - g₂).comp f = g₁.comp f - g₂.comp f