quotQuotEquivQuotSup_quot_quot_algebraMap

English

The algebra map quotQuotEquivQuotSupₐ respects the base algebra map to R: applying quotQuotEquivQuotSup to algebraMap x yields algebraMap x.

Русский

Алгебраическое отображение quotQuotEquivQuotSupₐ сохраняет базовую алгебраическую карту: применяя к algebraMap x получаем algebraMap x.

LaTeX

$$$DoubleQuot.quotQuotEquivQuotSupₐ (I,J) (algebraMap R _ x) = algebraMap _ _ x$$$

Lean4

@[simp]
theorem quotQuotEquivQuotSup_quot_quot_algebraMap (x : R) :
    DoubleQuot.quotQuotEquivQuotSup I J (algebraMap R _ x) = algebraMap _ _ x :=
  rfl

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