Commit 2025-11-25 01:06 0dd326c7

View on Github →

feat(translate): automatically infer the (reorder := ...) argument (#31902) This PR adds the feature to to_additive and to_dual that if the translation already exists (i.e. when using existing or self) the attribute will try to guess how to reorder the arguments correctly. If you then provide the same reorder argument manually, the linter will tell you that you can remove it.

Estimated changes

modified def Quiver.Hom.opEquiv
modified theorem le_of_not_ge
modified theorem le_or_gt
modified theorem le_total
modified theorem lt_iff_not_ge
modified theorem lt_of_not_ge
modified theorem lt_or_ge
modified theorem not_le
modified theorem not_lt
modified theorem le_of_eq
modified theorem le_of_lt
modified theorem not_le_of_gt
modified theorem not_lt_of_ge
added theorem le_imp_le'''
added theorem le_imp_le''
added theorem le_imp_le'
added theorem le_imp_le
added theorem not_lt_self
added theorem refl₁
added theorem refl₂