Theorems · Definition · general topology

ContinuousMap.tensorHom

{X : Type u_5} →
  {Y : Type u_6} →
    {R : Type u_7} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] → TensorProduct R C(X, R) C(Y, R) →ₗ[R] C(X × Y, R)

Tensor product version of ContinuousMap.prodMul.

Defined in

Mathlib.Topology.UniformSpace.ProdApproximation

Cited by

3 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRing