Theorem PiTensorProduct.equivPiTensorComplSingletonTensor_tprod

Modification history

2026-06-18 10:07
Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
feat(LinearAlgebra): generators of pi tensor products (#26464) …
Added PiTensorProduct.equivPiTensorComplSingletonTensor_tprodView on Github →