Def IsNoetherian.equivPUnitOfProdInjective

Modification history

2024-11-11 10:06
Mathlib/RingTheory/Noetherian/Defs.lean
chore(RingTheory/Noetherian): split `Noetherian.lean` (#18734) …
Modified IsNoetherian.equivPUnitOfProdInjectiveView on Github →
2024-06-04 13:17
Mathlib/RingTheory/Noetherian.lean
feat: left-Noetherian rings and commutative rings satisfy `OrzechProperty` (#13425) …
Added IsNoetherian.equivPUnitOfProdInjectiveView on Github →