Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-12 21:34 19dd4be3

View on Github →

chore(tactic/reserved_notation): change precedence of sup and inf (#10623) Put the precedence of and at 68 and 69 respectively, which is above + (65), and (67), and below * (70). This makes sure that inf and sup behave in the same way in expressions where arithmetic operations appear (which was not the case before). Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/inf.20and.20sup.20don't.20bind.20similarly

Estimated changes