Commit 2026-07-28 15:02 b595917d
View on Github →chore(LinearAlgebra/Pi): use Codisjoint, IsCompl (#42173)
... and syntactically generalise {I : Finset ι} to {I : Set ι} (hI : I.Finite). The new proofs also happen to not abuse the Set α := α → Prop defeq.