quotient_map_mkₐ

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.quotient_map_mkₐ

← MathLib Explorer

English

The mk map on the algebra level sends a to f(a) in the quotient level.

Русский

Карта mkₐ на уровне алгебр отправляет a → f(a) в частное.

LaTeX

$$$quotientMapₐ J f H (\operatorname{Quotient.mk I} a) = \operatorname{Quotient.mk_\!R_1 J}(f a)$$$

Lean4

@[simp]
theorem quotient_map_mkₐ (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) {x : A} :
    quotientMapₐ J f H (Quotient.mk I x) = Quotient.mkₐ R₁ J (f x) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru