@[simp]

theorem Ideal.Quotient.factorₐ_eq (R₁ : Type u_1) {A : Type u_2} [CommSemiring R₁] [Ring A] [Algebra R₁ A] {I : Ideal A} [I.IsTwoSided] : factorₐ R₁ ⋯ = AlgHom.id R₁ (A ⧸ I)