Theorem LinearMap.ext_on_codisjoint

Modification history

2024-06-08 08:17

Mathlib/Algebra/Module/Submodule/EqLocus.lean

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

Modified LinearMap.ext_on_codisjoint View on Github →

2023-07-15 18:30

Mathlib/LinearAlgebra/Basic.lean

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

Added LinearMap.ext_on_codisjoint View on Github →