ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometryEquiv.toLinearEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>f.toLinearEquiv = g.toLinearEquiv ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗ[σ₁₂] E₂<VAR>he : ∀ (x : E), ‖e x‖ = ‖x‖<GOAL>⇑{ toLinearEquiv := e, norm_map' := he } = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.toLinearEquiv = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e e' : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>h : ∀ (x : E), e x = e' x<GOAL>e = e'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x x' : E<GOAL>x = x' → f x = f x'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>h : f = g<VAR>x : E<GOAL>f x = g x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖e x‖ = ‖x‖
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometryEquiv.toLinearIsometry
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>f.toLinearIsometry = g.toLinearIsometry ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.toLinearIsometry = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Isometry ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometryEquiv.toIsometryEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.toIsometryEquiv = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Set.range ⇑e = Set.univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometryEquiv.toHomeomorph
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>f.toHomeomorph = g.toHomeomorph ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Continuous ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>ContinuousAt (⇑e) x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>ContinuousOn (⇑e) s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<VAR>x : E<GOAL>ContinuousWithinAt (⇑e) s x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometryEquiv.toContinuousLinearEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>f.toContinuousLinearEquiv = g.toContinuousLinearEquiv ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.toContinuousLinearEquiv = ⇑e
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>⇑(LinearIsometryEquiv.refl R E) = id
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E₂<GOAL>e (e.symm x) = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>e.symm (e x) = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>e x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.symm.symm = e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.symm = e.symm.toLinearEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.toIsometryEquiv.symm = e.symm.toIsometryEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.toHomeomorph.symm = e.symm.toHomeomorph
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>e₁ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>e₁ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃<VAR>c : E<GOAL>(e₁.trans e₂) c = e₂ (e₁ c)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃<GOAL>(e.trans e').toLinearEquiv = e.trans e'.toLinearEquiv
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.trans (LinearIsometryEquiv.refl R₂ E₂) = e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>(LinearIsometryEquiv.refl R E).trans e = e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.trans e.symm = LinearIsometryEquiv.refl R E
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.symm.trans e = LinearIsometryEquiv.refl R₂ E₂
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>e₁ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃<GOAL>(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>e₁ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃<GOAL>⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>E₄ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>Semiring R₄<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₁₃ : R →+* R₃<VAR>σ₃₁ : R₃ →+* R<VAR>σ₁₄ : R →+* R₄<VAR>σ₄₁ : R₄ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomInvPair σ₁₄ σ₄₁<VAR>RingHomInvPair σ₄₁ σ₁₄<VAR>RingHomInvPair σ₂₄ σ₄₂<VAR>RingHomInvPair σ₄₂ σ₂₄<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>RingHomCompTriple σ₄₂ σ₂₁ σ₄₁<VAR>RingHomCompTriple σ₄₃ σ₃₂ σ₄₂<VAR>RingHomCompTriple σ₄₃ σ₃₁ σ₄₁<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>SeminormedAddCommGroup E₄<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>Module R₄ E₄<VAR>eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃<VAR>eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄<GOAL>eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e e' : E ≃ₗᵢ[R] E<GOAL>⇑(e * e') = ⇑e ∘ ⇑e'
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e : E ≃ₗᵢ[R] E<GOAL>⇑e⁻¹ = ⇑e.symm
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>1 = LinearIsometryEquiv.refl R E
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e e' : E ≃ₗᵢ[R] E<GOAL>e * e' = e'.trans e
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e : E ≃ₗᵢ[R] E<GOAL>e⁻¹ = e.symm
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e.trans 1 = e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>LinearIsometryEquiv.trans 1 e = e
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e : E ≃ₗᵢ[R] E<GOAL>LinearIsometryEquiv.refl R E * e = e
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>e : E ≃ₗᵢ[R] E<GOAL>e * LinearIsometryEquiv.refl R E = e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>⇑↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>e 0 = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>e (x + y) = e x + e y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>e (x - y) = e x - e y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>c : R<VAR>x : E<GOAL>e (c • x) = σ₁₂ c • e x
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R E₂<VAR>e : E ≃ₗᵢ[R] E₂<VAR>c : R<VAR>x : E<GOAL>e (c • x) = c • e x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖e x‖₊ = ‖x‖₊
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>dist (e x) (e y) = dist x y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>edist (e x) (e y) = edist x y