Theorem LinearMap.eqOn_span

Modification history

2023-07-15 18:30

Mathlib/LinearAlgebra/Span.lean

refactor: use `SemilinearMapClass` in `LinearMap.eqLocus` (#5929) …

Modified LinearMap.eqOn_span View on Github →

2023-02-14 14:29

Mathlib/LinearAlgebra/Span.lean

feat: port LinearAlgebra.Span (#2248)

Added LinearMap.eqOn_span View on Github →