Theorem TensorProduct.ext_iff_inner_right_threefold'

Modification history

2025-10-16 16:17
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
feat(Analysis/InnerProductSpace): define the inner product on tensor products (#27228) …
Added TensorProduct.ext_iff_inner_right_threefold'View on Github →