Commit 2025-11-13 23:13 2b55585f

View on Github →

feat: to_dual attribute (#27887) This PR defines the to_dual attribute for translating lemmas to their dual. This is useful in order theory and in category theory. It is built on top of the to_additive machinery. This PR only adds @[to_dual] tags in files that directly need to import ToDual, namely Order/Defs/PartialOrder, Order/Notation and Combinatorics/Quiver/Basic. Further tagging is left for (many) future PRs. This PR continues the work from #21719 Related (mathlib3) issues:

Estimated changes

modified theorem Quiver.eq_homOfEq_iff
modified theorem Quiver.heq_of_homOfEq_ext
modified def Quiver.homOfEq
modified theorem Quiver.homOfEq_eq_iff
modified theorem Quiver.homOfEq_heq
modified theorem Quiver.homOfEq_heq_left_iff
modified theorem Quiver.homOfEq_injective
modified theorem Quiver.homOfEq_rfl
modified theorem Quiver.homOfEq_trans
deleted theorem ge_antisymm
deleted theorem ge_of_eq
deleted theorem lt_of_le_of_ne'
deleted theorem lt_or_eq_of_le'
deleted theorem ge_trans
deleted theorem gt_trans
modified theorem le_trans
modified theorem lt_irrefl
deleted theorem lt_of_le_of_lt'
deleted theorem lt_of_lt_of_le'
deleted theorem ne_of_gt
deleted def List.swapFirstTwo
deleted theorem ToAdditive.Pow_lemma
deleted theorem ToAdditive.mul_comm'
deleted theorem ToAdditive.mul_one'
deleted structure ToAdditive.will.ArgInfo
deleted structure ToAdditive.will.Config
deleted def ToAdditive.nameDict