The opposite of a commutative Noetherian ring

Right modules over a ring A are modules over Aᵐᵒᵖ, so categories of finitely generated right modules ask for IsNoetherianRing Aᵐᵒᵖ. For a commutative ring, RingEquiv.toOpposite identifies A with Aᵐᵒᵖ, and this file records the resulting instance, so that the right Noetherian hypothesis is found automatically for commutative Noetherian rings.

instance MulOpposite.isNoetherianRing {R : Type u_1} [CommSemiring R] [IsNoetherianRing R] : IsNoetherianRing Rᵐᵒᵖ

The opposite of a commutative Noetherian semiring is Noetherian.