Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-21 10:53 d5653736

View on Github →

feat(order/galois_connection, linear_algebra/basic): x ∈ R ∙ y is a transitive relation (#10943)

Estimated changes