quotQuotEquivQuotOfLEₐ_toRingEquiv

English

If I ≤ J is the inclusion of ideals, then the isomorphism quotQuotEquivQuotOfLEₐ R h is equal to quotQuotEquivQuotOfLE h when viewed as a ring equivalence.

Русский

При включении идеалов I ≤ J существует изоморфизм quotQuotEquivQuotOfLEₐ R h; если рассматривать его как кольцевое эквивалентности, он совпадает с quotQuotEquivQuotOfLE h.

LaTeX

$$$((quotQuotEquivQuotOfLEₐ R h) : _ ≃+* _) = quotQuotEquivQuotOfLE h$$$

Lean4

@[simp]
theorem quotQuotEquivQuotOfLEₐ_toRingEquiv (h : I ≤ J) :
    (quotQuotEquivQuotOfLEₐ R h : _ ⧸ J.map (Quotient.mkₐ R I) ≃+* _) = quotQuotEquivQuotOfLE h :=
  rfl

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