Theorem LinearPMap.supSpanSingleton_apply_mk_of_mem

Modification history

2026-04-03 14:10

Mathlib/LinearAlgebra/LinearPMap.lean

refactor(LinearAlgebra/LinearPMap): generalize (partially) to semilinear maps (#36721) …

Modified LinearPMap.supSpanSingleton_apply_mk_of_mem View on Github →

2025-05-05 08:35

Mathlib/LinearAlgebra/LinearPMap.lean

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

Added LinearPMap.supSpanSingleton_apply_mk_of_mem View on Github →