ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalAddGroup M<VAR>z : ℤ<VAR>m : M<GOAL>↑z m = z • m
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>TopologicalRing R<VAR>c : R<VAR>n : ℕ<GOAL>ContinuousLinearMap.smulRight 1 c ^ n = ContinuousLinearMap.smulRight 1 (c ^ n)
<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>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>TopologicalAddGroup M<VAR>f₁ : M →SL[σ₁₂] M₂<VAR>f₂ : M₂ →SL[σ₂₁] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>x : M<GOAL>↑((f₁.projKerOfRightInverse f₂ h) x) = x - f₂ (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>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>TopologicalAddGroup M<VAR>f₁ : M →SL[σ₁₂] M₂<VAR>f₂ : M₂ →SL[σ₂₁] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>x : ↥(LinearMap.ker f₁)<GOAL>(f₁.projKerOfRightInverse f₂ h) ↑x = 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>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>TopologicalAddGroup M<VAR>f₁ : M →SL[σ₁₂] M₂<VAR>f₂ : M₂ →SL[σ₂₁] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>y : M₂<GOAL>(f₁.projKerOfRightInverse f₂ h) (f₂ y) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace R<VAR>DivisionRing R<VAR>ContinuousSub R<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>f : M →L[R] R<VAR>hf : f ≠ 0<GOAL>IsOpenMap ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>S₃ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>Monoid S₃<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>M₃ : Type u_8<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₃ M₃<VAR>DistribMulAction S₃ M₃<VAR>SMulCommClass R₃ S₃ M₃<VAR>ContinuousConstSMul S₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>c : S₃<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>f : M →SL[σ₁₂] M₂<GOAL>(c • h).comp f = c • h.comp f
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>Semiring R<VAR>Monoid S<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₂ : Type u_9<VAR>TopologicalSpace N₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>DistribMulAction S N₃<VAR>SMulCommClass R S N₃<VAR>ContinuousConstSMul S N₃<VAR>DistribMulAction S N₂<VAR>ContinuousConstSMul S N₂<VAR>SMulCommClass R S N₂<VAR>LinearMap.CompatibleSMul N₂ N₃ S R<VAR>hₗ : N₂ →L[R] N₃<VAR>c : S<VAR>fₗ : M →L[R] N₂<GOAL>hₗ.comp (c • fₗ) = c • hₗ.comp fₗ
<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>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>M₃ : Type u_8<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>SMulCommClass R₂ R₂ M₂<VAR>SMulCommClass R₃ R₃ M₃<VAR>ContinuousConstSMul R₂ M₂<VAR>ContinuousConstSMul R₃ M₃<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>c : R₂<VAR>f : M →SL[σ₁₂] M₂<GOAL>h.comp (c • f) = σ₂₃ c • h.comp 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>N₂ : Type u_9<VAR>TopologicalSpace N₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>f : (M →L[R] N₂) × (M →L[R] N₃)<GOAL>ContinuousLinearMap.prodEquiv f = f.1.prod f.2
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₂ : Type u_9<VAR>TopologicalSpace N₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>f g : M × N₂ →L[R] N₃<GOAL>f = g ↔ f.comp (ContinuousLinearMap.inl R M N₂) = g.comp (ContinuousLinearMap.inl R M N₂) ∧ f.comp (ContinuousLinearMap.inr R M N₂) = g.comp (ContinuousLinearMap.inr R M N₂)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₂ : Type u_9<VAR>TopologicalSpace N₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>f g : M × N₂ →L[R] N₃<VAR>hl : f.comp (ContinuousLinearMap.inl R M N₂) = g.comp (ContinuousLinearMap.inl R M N₂)<VAR>hr : f.comp (ContinuousLinearMap.inr R M N₂) = g.comp (ContinuousLinearMap.inr R M N₂)<GOAL>f = g
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>Semiring R<VAR>Semiring S<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₂ : Type u_9<VAR>TopologicalSpace N₂<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>Module S N₂<VAR>ContinuousConstSMul S N₂<VAR>SMulCommClass R S N₂<VAR>Module S N₃<VAR>SMulCommClass R S N₃<VAR>ContinuousConstSMul S N₃<VAR>ContinuousAdd N₂<VAR>ContinuousAdd N₃<GOAL>∀ (a : (M →L[R] N₂) × (M →L[R] N₃)), (ContinuousLinearMap.prodₗ S) a = ContinuousLinearMap.prodEquiv.toFun a
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>Semiring R<VAR>Semiring S<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>N₃ : Type u_10<VAR>TopologicalSpace N₃<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>Module S N₃<VAR>SMulCommClass R S N₃<VAR>ContinuousConstSMul S N₃<VAR>ContinuousAdd N₃<VAR>self : M →L[R] N₃<GOAL>(ContinuousLinearMap.coeLM S) self = ↑self
<VAR>R : Type u_1<VAR>R₃ : Type u_3<VAR>S₃ : Type u_5<VAR>Semiring R<VAR>Semiring R₃<VAR>Semiring S₃<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₃ : Type u_8<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₃ M₃<VAR>Module S₃ M₃<VAR>SMulCommClass R₃ S₃ M₃<VAR>ContinuousConstSMul S₃ M₃<VAR>σ₁₃ : R →+* R₃<VAR>ContinuousAdd M₃<VAR>self : M →SL[σ₁₃] M₃<GOAL>(ContinuousLinearMap.coeLMₛₗ σ₁₃) self = ↑self
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring S<VAR>Semiring T<VAR>Module R S<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Module S M₂<VAR>IsScalarTower R S M₂<VAR>TopologicalSpace S<VAR>TopologicalSpace M₂<VAR>ContinuousSMul S M₂<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousAdd M₂<VAR>Module T M₂<VAR>ContinuousConstSMul T M₂<VAR>SMulCommClass R T M₂<VAR>SMulCommClass S T M₂<VAR>c : M →L[R] S<GOAL>⇑c.smulRightₗ = c.smulRight
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>TopologicalAddGroup M₂<VAR>ContinuousConstSMul R M₂<VAR>r : R<VAR>m : M₂<GOAL>((algebraMap R (M₂ →L[R] M₂)) r) m = r • m
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>f : M →L[A] M₂<GOAL>↑(ContinuousLinearMap.restrictScalars R f) = ↑R ↑f
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>f : M →L[A] M₂<GOAL>⇑(ContinuousLinearMap.restrictScalars R f) = ⇑f
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<GOAL>ContinuousLinearMap.restrictScalars R 0 = 0
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>TopologicalAddGroup M₂<VAR>f g : M →L[A] M₂<GOAL>ContinuousLinearMap.restrictScalars R (f + g) = ContinuousLinearMap.restrictScalars R f + ContinuousLinearMap.restrictScalars R g
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>TopologicalAddGroup M₂<VAR>f : M →L[A] M₂<GOAL>ContinuousLinearMap.restrictScalars R (-f) = -ContinuousLinearMap.restrictScalars R f
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>S : Type u_5<VAR>Ring S<VAR>Module S M₂<VAR>ContinuousConstSMul S M₂<VAR>SMulCommClass A S M₂<VAR>SMulCommClass R S M₂<VAR>c : S<VAR>f : M →L[A] M₂<GOAL>ContinuousLinearMap.restrictScalars R (c • f) = c • ContinuousLinearMap.restrictScalars R f
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring A<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module A M<VAR>Module A M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>R : Type u_4<VAR>Ring R<VAR>Module R M<VAR>Module R M₂<VAR>LinearMap.CompatibleSMul M M₂ R A<VAR>S : Type u_5<VAR>Ring S<VAR>Module S M₂<VAR>ContinuousConstSMul S M₂<VAR>SMulCommClass A S M₂<VAR>SMulCommClass R S M₂<VAR>TopologicalAddGroup M₂<GOAL>⇑(ContinuousLinearMap.restrictScalarsₗ A M M₂ R S) = ContinuousLinearMap.restrictScalars R
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>b : M₁<GOAL>↑e b = e b
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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₂<GOAL>⇑f.toLinearEquiv = ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>⇑↑e = ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>Function.Injective ContinuousLinearEquiv.toLinearEquiv
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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 g : M₁ ≃SL[σ₁₂] M₂<VAR>h : ⇑f = ⇑g<GOAL>f = g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>Function.Injective ContinuousLinearEquiv.toContinuousLinearMap
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e e' : M₁ ≃SL[σ₁₂] M₂<GOAL>↑e = ↑e' ↔ e = e'
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>IsOpenMap ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>⇑e '' closure s = closure (⇑e '' s)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₂<GOAL>⇑e ⁻¹' closure s = closure (⇑e ⁻¹' s)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>IsClosed (⇑e '' s) ↔ IsClosed s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>Filter.map (⇑e) (𝓝 x) = 𝓝 (e x)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>e 0 = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>x y : M₁<GOAL>e (x + y) = e x + e y
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>c : R₁<VAR>x : M₁<GOAL>e (c • x) = σ₁₂ c • e 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>e : M₁ ≃L[R₁] M₂<VAR>c : R₁<VAR>x : M₁<GOAL>e (c • x) = c • e x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>e x = 0 ↔ x = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>Continuous ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>ContinuousOn (⇑e) s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>ContinuousAt (⇑e) x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<VAR>x : M₁<GOAL>ContinuousWithinAt (⇑e) s x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>α : Type u_9<VAR>TopologicalSpace α<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>f : α → M₁<VAR>s : Set α<GOAL>ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>α : Type u_9<VAR>TopologicalSpace α<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>f : α → M₁<GOAL>Continuous (⇑e ∘ f) ↔ Continuous 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>TopologicalSpace R₁<VAR>f g : R₁ ≃L[R₁] M₁<VAR>h : f 1 = g 1<GOAL>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₁<GOAL>↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<GOAL>⇑(ContinuousLinearEquiv.refl R₁ M₁) = id
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>e.symm.toLinearEquiv = e.symm
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<GOAL>e.toHomeomorph.symm = e.symm.toHomeomorph
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<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>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>Filter.map (⇑e.symm) (𝓝 (e x)) = 𝓝 x
<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>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<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>e₁ : M₁ ≃SL[σ₁₂] M₂<VAR>e₂ : M₂ ≃SL[σ₂₃] M₃<GOAL>(e₁.trans e₂).toLinearEquiv = e₁.trans e₂.toLinearEquiv
<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>e : M₁ ≃L[R₁] M₂<VAR>e' : M₃ ≃L[R₁] M₄<VAR>x : M₁ × M₃<GOAL>(e.prod e') x = (e x.1, e' 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>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>e : M₁ ≃L[R₁] M₂<VAR>e' : M₃ ≃L[R₁] M₄<GOAL>↑(e.prod e') = (↑e).prodMap ↑e'
<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>e : M₁ ≃L[R₁] M₂<VAR>e' : M₃ ≃L[R₁] M₄<GOAL>(e.prod e').symm = e.symm.prod e'.symm
<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>(ContinuousLinearEquiv.prodComm R₁ M₁ M₂).toLinearEquiv = LinearEquiv.prodComm 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>∀ (a : M₁ × M₂), (ContinuousLinearEquiv.prodComm R₁ M₁ M₂) a = a.swap
<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>(ContinuousLinearEquiv.prodComm R₁ M₁ M₂).symm = ContinuousLinearEquiv.prodComm R₁ M₂ M₁