Quotient_Ring_of_Commutative_Ring_is_Commutative
Provedproofwikiquotient-rings
If R is a commutative ring and J an ideal, then R/J is also commutative.
Preamble
import Mathlib.RingTheory.Ideal.Quotient.Basic
Formal statement
theorem Quotient_Ring_of_Commutative_Ring_is_Commutative {R : Type _} [CommRing R] (J : Ideal R) : ∀ a b : R ⧸ J, a * b = b * a := by sorrySource