Theorems · Theorem · general topology
ContinuousMap.tensorHom_tmul
∀ {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] (f : C(X, R)) (g : C(Y, R)),
ContinuousMap.tensorHom (f ⊗ₜ[R] g) = (ContinuousMap.prodMul f) g- Cited by
- 1 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- RingHom.idstatement and proof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapstatement and proof · cited by 10,215
- TensorProductstatement and proof · cited by 2,545
- ContinuousMapstatement and proof · cited by 2,491
- TensorProduct.tmulstatement and proof · cited by 1,182
- IsTopologicalRingstatement and proof · cited by 402
- TensorProduct.lift.tmulproof · cited by 8
- ContinuousMap.prodMulstatement and proof · cited by 4
- ContinuousMap.tensorHomstatement · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- AbstractMeasure.prodMk_eq_prodMk'proof · cited by 0