quotQuotEquivComm_algebraMap — Mathlib

English

The quotQuotEquivComm_algebraMap statement asserts that quotQuotEquivComm I J sends algebraMap from R to the final double-quotient to the same algebraMap, i.e., the isomorphism respects the base embedding.

Русский

Утверждение quotQuotEquivComm_algebraMap: изоморфизм quotQuotEquivComm I J сохраняет базовое вложение R в итоговый двойной фактор, отображая algebraMap как есть.

LaTeX

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

Lean4

@[simp]
theorem quotQuotEquivComm_algebraMap (x : R) : quotQuotEquivComm I J (algebraMap R _ x) = algebraMap _ _ x :=
  rfl

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