Theorem dualTensorHom_bijective

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 dualTensorHom_bijective View on Github →

2026-07-16 14:39

Mathlib/LinearAlgebra/Contraction.lean

feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to `CommSemiring` (#40297) …

Added dualTensorHom_bijective View on Github →