Theorem LinearMap.ext_on_range

Modification history

2025-12-27 09:40
Mathlib/LinearAlgebra/Span/Basic.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified LinearMap.ext_on_rangeView on Github →
2024-04-23 01:17
Mathlib/LinearAlgebra/Span.lean
fix: generalize index types of `iSup` to Sort (#12114) …
Modified LinearMap.ext_on_rangeView on Github →
2023-08-10 19:52
Mathlib/LinearAlgebra/Span.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified LinearMap.ext_on_rangeView on Github →
2023-07-15 18:30
Mathlib/LinearAlgebra/Span.lean
refactor: use `SemilinearMapClass` in `LinearMap.eqLocus` (#5929) …
Modified LinearMap.ext_on_rangeView on Github →
2023-02-14 14:29
Mathlib/LinearAlgebra/Span.lean
feat: port LinearAlgebra.Span (#2248)
Added LinearMap.ext_on_rangeView on Github →