Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
bug (Mathlib.Data.Finset.Sym) : suppress global variable (m : Sym alp…
…ha n) (#10637) A global `variable {m : Sym α n}` was present in `Mathlib.Data.Finset.Sym` with the very unfortunate effect that docs#Finset.sym_eq_empty was using it : ``` theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} : Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅ ``` thus making it impossible to use to prove its goal. The line is modified, added in a few functions when needed. Co-authored-by: Antoine Chambert-Loir <[email protected]>
- Loading branch information