Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-13 12:20 32c2768b

View on Github →

chore(linear_algebra/basic): simplify two proofs (#2123)

  • chore(linear_algebra/basic): simplify two proofs Also drop linear_map.congr_right in favor of linear_equiv.congr_right. I'll restore the deleted congr_right as comp_map : (M₂ →ₗ[R] M₃) →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃) soon.
  • Fix compile
  • Restore congr_right under the name comp_right.

Estimated changes

modified def linear_equiv.conj