Theorem Module.Projective.of_one_mem_range_dualTensorHom

Modification history

2026-07-16 14:39
Mathlib/LinearAlgebra/Contraction.lean
feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to `CommSemiring` (#40297) …
Added Module.Projective.of_one_mem_range_dualTensorHomView on Github →