quotientEquivAlgOfEq — Mathlib

English

If I and J are two-sided ideals of A and I = J, then the quotients A/I and A/J are isomorphic as algebras over the base ring.

Русский

Если I и J — двусторонние идеалы A и I = J, то частоты A/I и A/J изоморфны как алгебры над базовым кольцом.

LaTeX

$$$(A/I) \\cong_{R} (A/J)$$$

Lean4

/-- Quotienting by equal ideals gives equivalent algebras. -/
def quotientEquivAlgOfEq {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) : (A ⧸ I) ≃ₐ[R₁] A ⧸ J :=
  quotientEquivAlg I J AlgEquiv.refl <| h ▸ (map_id I).symm

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