mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(LinearAlgebra/TensorProduct/Basic): add some results on `TensorProduct.congr`

Open acmepjz opened this issue 1 year ago • 0 comments

  • TensorProduct.congr_symm which states (TensorProduct.congr f g).symm = TensorProduct.congr f.symm g.symm
  • TensorProduct.coe_congr_(left|right)_refl: relates TensorProduct.congr and LinearMap.(l|r)Tensor

Open in Gitpod

acmepjz avatar Mar 27 '24 19:03 acmepjz