Commit 2022-05-05 13:10 929c9018

View on Github →

refactor(ring_theory/*): Remove unnecessary commutativity assumptions (#13966) This replaces [comm_ring R] or [comm_semiring R] with [ring R] or [semiring R], without changing any proofs.

Estimated changes

Modified src/ring_theory/artinian.lean

modified theorem is_artinian_ring_of_ring_equiv

modified theorem is_artinian_ring_of_surjective

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/ideal/basic.lean

modified theorem ideal.maximal_of_no_maximal

Modified src/ring_theory/noetherian.lean

modified theorem is_noetherian_ring_iff_ideal_fg

modified theorem is_noetherian_ring_of_ring_equiv

modified theorem is_noetherian_ring_of_surjective

modified theorem submodule.fg_restrict_scalars