Theorem PiTensorProduct.subsingletonEquiv_symm_apply'

Modification history

2025-12-11 10:09
Mathlib/LinearAlgebra/PiTensorProduct.lean
feat(LinearAlgebra/PiTensorProduct): add version of `subsingletonEquiv` for dependent case (#32598) …
Added PiTensorProduct.subsingletonEquiv_symm_apply'View on Github →