English
If two semirings are equivalent and their quotients by a relation are defined, then the quotients are equivalent.
Русский
Если два полупрямых кольца эквивалентны и их частные по отношению к отношению определены, то и их частные эквивалентны.
LaTeX
$$$\\text{equivQuotEquiv }(f, rel)$$$
Lean4
/-- If two (semi)rings are equivalent and their quotients by a relation `rel` are defined,
then their quotients are also equivalent.
(Special case of `algEquiv_quot_algEquiv` when `R = ℕ`, which in turn is a special
case of the third isomorphism theorem.) -/
def equivQuotEquiv {A B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : A → A → Prop) :
RingQuot rel ≃+* RingQuot (rel on f.symm) :=
let f_alg : A ≃ₐ[ℕ] B := AlgEquiv.ofRingEquiv (f := f) (fun n ↦ by simp)
algEquivQuotAlgEquiv f_alg rel |>.toRingEquiv
