From b1096710aaf0f33a8c37eb0d7c8b2bcb7bf586b7 Mon Sep 17 00:00:00 2001 From: Lukas Miaskiwskyi Date: Mon, 30 Jan 2023 16:38:29 +0000 Subject: [PATCH] fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn (#1946) A misaligned `to_additive` causes some proofs to fail in #1911. No backport needed, the misalign happened due to a mathlib4 exclusive mistake as I understand. --- Mathlib/Data/Set/Pointwise/ListOfFn.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Pointwise/ListOfFn.lean b/Mathlib/Data/Set/Pointwise/ListOfFn.lean index c93b3c4f1bfd0..ccfc0dec6ee1e 100644 --- a/Mathlib/Data/Set/Pointwise/ListOfFn.lean +++ b/Mathlib/Data/Set/Pointwise/ListOfFn.lean @@ -55,10 +55,11 @@ theorem mem_list_prod {l : List (Set α)} {a : α} : #align set.mem_list_prod Set.mem_list_prod #align set.mem_list_sum Set.mem_list_sum -@[to_additive mem_mul] +@[to_additive] theorem mem_pow {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a := by rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate] #align set.mem_pow Set.mem_pow +#align set.mem_nsmul Set.mem_nsmul end Set