Theorem IsNoetherian.subsingleton_of_prod_injective

Modification history

2024-11-11 10:06

Mathlib/RingTheory/Noetherian/Defs.lean

chore(RingTheory/Noetherian): split `Noetherian.lean` (#18734) …

Modified IsNoetherian.subsingleton_of_prod_injective View on Github →

2024-06-04 13:17

Mathlib/RingTheory/Noetherian.lean

feat: left-Noetherian rings and commutative rings satisfy `OrzechProperty` (#13425) …

Added IsNoetherian.subsingleton_of_prod_injective View on Github →