quotQuotEquivComm_mk_mk — Mathlib

English

For any commutative ring R and ideals I,J of A, the map quotQuotEquivComm I J acts trivially on the embedded image of R, sending algebraMap(x) to algebraMap(x).

Русский

Для любых R и идеалов I,J в A отображение quotQuotEquivComm I J сохраняет образ R, отправляя algebraMap(x) в algebraMap(x).

LaTeX

$$$quotQuotEquivComm I J (algebraMap R _ x) = algebraMap _ _ x$$$

Lean4

@[simp]
theorem quotQuotEquivComm_mk_mk [CommRing R] (I J : Ideal R) (x : R) :
    quotQuotEquivComm I J (Ideal.Quotient.mk _ (Ideal.Quotient.mk _ x)) = algebraMap R _ x :=
  rfl

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