Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-10 04:04 3aad7f1e

View on Github →

feat(data/matrix/pequiv): partial equivalences to represent matrices (#1228)

  • feat(matrix/pequiv): partial equivalences to represent matrices
  • use notation for pequiv
  • correct imports
  • finish correcting imports
  • add some docs
  • Add documentation
  • improve documentation

Estimated changes

added def pequiv.to_matrix
added theorem pequiv.to_matrix_bot
added theorem pequiv.to_matrix_refl
added theorem pequiv.to_matrix_swap
added theorem pequiv.to_matrix_symm
added theorem pequiv.to_matrix_trans