quotientEquivAlgOfEq_mk — Mathlib

English

If I and J are two-sided ideals of A and h: I = J, then the quotient equivalence quotientEquivAlgOfEq R h identifies the classes consistently.

Русский

Если I и J — двусторонние идеалы A и h: I = J, то эквивалентность частот quotientEquivAlgOfEq R h согласованно идентифицирует классы.

LaTeX

$$$(A/I) \\equiv_{R} (A/J)$ with the canonical map sending \\overline{x}^I \\mapsto \\overline{x}^J$$$

Lean4

@[simp]
theorem quotientEquivAlgOfEq_mk {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) (x : A) :
    quotientEquivAlgOfEq R₁ h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
  rfl

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