Theorem LinearMap.submoduleOf_span_singleton_of_mem

Modification history

2025-05-03 07:23
Mathlib/LinearAlgebra/Span/Basic.lean
feat(Algebra): finiteness of associated primes (#24242) …
Added LinearMap.submoduleOf_span_singleton_of_memView on Github →