Theorem IsNoetherian.subsingleton_of_injective

Modification history

2025-12-19 08:36
Mathlib/RingTheory/Noetherian/Basic.lean
feat(LinearAlgebra): more on StrongRankCondition (#32194) …
Added IsNoetherian.subsingleton_of_injectiveView on Github →