Theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse
Modification history
2026-09-03 07:46
Mathlib/LinearAlgebra/Contraction.lean
feat(LinearAlgebra): dual of tensor is tensor of duals for finite projective modules (#41479) …
Modified TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverseView on Github →