Commit 2025-01-28 00:34 8959d573

View on Github →

feat(Matrix): more lemmas for PEquiv.toMatrix (#21143) Also

  • add Matrix.transpose_stdBasisMatrix and conjTranspose version
  • add Matrix.ext_ofMulVec
  • tag Matrix.GeneralLinearGroup.map with @[simps] From "Formalizing the Bruhat-Tits tree" Co-authored by: Judith Ludwig ludwig@mathi.uni-heidelberg.de

Estimated changes

added theorem PEquiv.map_toMatrix