quotientEquivAlg — Mathlib

English

The algebra equivalence between A/I and B/J is 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 $f$ with $J = f(I)$$$

Lean4

/-- The algebra equiv `A/I ≃ₐ[R] B/J` induced by an algebra equiv `f : A ≃ₐ[R] B`,
where`J = f(I)`. -/
def quotientEquivAlg (f : A ≃ₐ[R₁] B) (hIJ : J = I.map (f : A →+* B)) : (A ⧸ I) ≃ₐ[R₁] B ⧸ J :=
  { quotientEquiv I J (f : A ≃+* B) hIJ with commutes' r := by simp }

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