Commit 2026-05-20 14:21 aefd5531

refactor(Data/Finsupp): use single in uniqueEquiv (#37755) In essence, this changes (Finsupp.uniqueEquiv i).symm m from having support univ.filter (fun _ ↦ m ≠ 0) to having support if m = 0 then {i} else ∅. These are equal, but having the RHS be single 1 r is much more useful in practice. Similarly for MonoidAlgebra. To avoid simp getting stuck after rewriting with uniqueEquiv_symm_apply, add uniqueEquiv_symm_apply_apply and tag it with simp↓ high. Also rename Equiv.finsuppUnique to Finsupp.uniqueEquiv and change the Unique ι argument into Subsingleton ι and i : ι. Similarly for AddEquiv and LinearEquiv.