Commit 2026-09-03 07:46 e21ec050

feat(LinearAlgebra): dual of tensor is tensor of duals for finite projective modules (#41479) Generalise this isomorphism and many similar ones from finite free to finite projective. To be able to deduce some isos from some other ones, I had to move them around in a preliminary PR. Note that #40297 made of the changes that the current PR was intending to do but not all, hence the slightly mangled diff. Also change the defeq of homTensorHomEquiv so that it is not defeq to homTensorHomMap (but would be if homTensorHomMap became heterobasic). This makes BilinForm.tensorDistribEquiv defeq to BilinForm.tensorDistrib. Also tag LinearEquiv.congrRight with simps to generate some required simp lemmas. Human generated then golfed and edited with Claude Opus, then human-edited some more. From FLT, PersistentDecomp Assisted-by: Claude Opus 4.8