Commit 2025-07-19 04:00 6aa7f2e0

View on Github →

feat(LinearAlgebra): lemmas about LinearPMap.sSup domain (#27054) Two small lemmas so one doesn't need to unfold the definition

Estimated changes

added theorem LinearPMap.domain_sSup