Theorem Finsupp.mapRange_eq_zero

Modification history

2025-12-09 04:22

Mathlib/Data/Finsupp/Defs.lean

refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)

Added Finsupp.mapRange_eq_zero View on Github →