Quotient_Ring_Product_is_Well_Defined
Provedproofwikiquotient-rings
Let R be a ring, J an ideal. Then multiplication is well-defined on R/J: if x₁ + J = x₂ + J and y₁ + J = y₂ + J then x₁y₁ + J = x₂y₂ + J.
Preamble
import Mathlib.RingTheory.Ideal.Quotient.Basic
Formal statement
theorem Quotient_Ring_Product_is_Well_Defined {R : Type _} [CommRing R] (J : Ideal R) (x₁ x₂ y₁ y₂ : R) (hx : Ideal.Quotient.mk J x₁ = Ideal.Quotient.mk J x₂) (hy : Ideal.Quotient.mk J y₁ = Ideal.Quotient.mk J y₂) : Ideal.Quotient.mk J (x₁ * y₁) = Ideal.Quotient.mk J (x₂ * y₂) := by sorrySource