Commit 2025-05-05 08:35 a3652388

View on Github →

feat(LinearPMap): more lemmas about supSpanSingleton (#23231)

Estimated changes

Modified Mathlib/LinearAlgebra/LinearPMap.lean

added theorem LinearPMap.supSpanSingleton_apply_mk_of_mem

added theorem LinearPMap.supSpanSingleton_apply_of_mem

added theorem LinearPMap.supSpanSingleton_apply_self

added theorem LinearPMap.supSpanSingleton_apply_smul_self

Modified Mathlib/LinearAlgebra/Span/Defs.lean