Theorem Matrix.intCast_apply

Modification history

2025-12-09 04:22
Mathlib/Data/Matrix/Diagonal.lean
refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)
Added Matrix.intCast_applyView on Github →