Skip to content

Commit

Permalink
fix: misaligned to_additive in Data/Set/Pointwise/ListOfFn (#1946)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
LukasMias committed Jan 30, 2023
1 parent ce69064 commit b109671
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Mathlib/Data/Set/Pointwise/ListOfFn.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit b109671

Please sign in to comment.