Def LinearMap.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.eqLocus View on Github →

2023-07-15 18:30

Mathlib/LinearAlgebra/Basic.lean

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

Modified LinearMap.eqLocus View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added LinearMap.eqLocus View on Github →