quotientEquiv_mk — Mathlib

English

There is an algebra equivalence between A/ I and B/ J induced by an algebra equivalence f with J = f(I).

Русский

Существует алгебраическое эквивалентное отображение между A/I и B/J, индуцированное алгебраическим эквивалентом f, когда J = f(I).

LaTeX

$$$ (A/I) \simeq_A (B/J) $ via quotientEquivAlg f hIJ$$

Lean4

theorem quotientEquiv_mk (x : R) : quotientEquiv I J f hIJ (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J (f x) :=
  rfl

Похожие утверждения