Theorem LinearMap.le_eqLocus

Modification history

2024-06-08 08:17

Mathlib/Algebra/Module/Submodule/EqLocus.lean

chore: move LinearMap.eqLocus to its own file (#13566)

Modified LinearMap.le_eqLocus View on Github →

2023-07-15 18:30

Mathlib/LinearAlgebra/Basic.lean

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

Added LinearMap.le_eqLocus View on Github →