From f7607b021f0575620e68d308e6ae1bebc761f947 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 25 May 2026 11:27:23 +0200 Subject: [PATCH 1/2] feat: document the `@[to_additive]`/`@[to_dual]` policy --- templates/contribute/style.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/templates/contribute/style.md b/templates/contribute/style.md index 56001c480..ba2b0a710 100644 --- a/templates/contribute/style.md +++ b/templates/contribute/style.md @@ -311,6 +311,12 @@ theorem Ordinal.sub_eq_zero_iff_le {a b : Ordinal} : a - b = 0 ↔ a ≤ b := fun h => by rwa [← Ordinal.le_zero, sub_le, add_zero]⟩ ``` +The `@[to_additive]` and `@[to_dual]` attributes are pieces of automation +that respectively generate additive versions of algebraic multiplicative +statements and dualised versions of order theoretic statements. +Where applicable, these attributes should be used +over writing the second statement by hand. + ### Instances When providing terms of structures or instances of classes, the `where` From 8e8527d4b531edb8be7f71404ee4c0c38256492b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 26 May 2026 11:59:29 +0200 Subject: [PATCH 2/2] examples and mention category theory --- templates/contribute/style.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/templates/contribute/style.md b/templates/contribute/style.md index ba2b0a710..e7515a603 100644 --- a/templates/contribute/style.md +++ b/templates/contribute/style.md @@ -313,9 +313,17 @@ theorem Ordinal.sub_eq_zero_iff_le {a b : Ordinal} : a - b = 0 ↔ a ≤ b := The `@[to_additive]` and `@[to_dual]` attributes are pieces of automation that respectively generate additive versions of algebraic multiplicative -statements and dualised versions of order theoretic statements. +statements and dualised versions of order/category theoretic statements. Where applicable, these attributes should be used over writing the second statement by hand. +```lean +@[to_additive] -- generates `add_rotate` +theorem mul_rotate {G : Type*} (a b c : G) : a * b * c = b * c * a := sorry + +-- `to_additive` can't be used here because `ℝ` can't be additivised. +theorem mul_rotate' (a b c : ℝ) : a * b * c = b * c * a := sorry +``` + ### Instances