Commit 2023-12-13 18:20 c4988d10

View on Github →

feat: make isNoetherian_of_isNoetherianRing_of_finite an instance (#8999) Make isNoetherian_of_isNoetherianRing_of_finite an instance: this was impossible in Lean 3 because of a loop.

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/Probability/Cdf.lean

Modified Mathlib/RingTheory/Adjoin/Tower.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/Noetherian.lean

deleted theorem isNoetherian_of_isNoetherianRing_of_finite