Commit 2024-02-16 16:23 cf6053db

bug (Mathlib.Data.Finset.Sym) : suppress global variable (m : Sym alpha 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.