quotientQuotientEquivQuotientAux_mk_mk

Mathlib.LinearAlgebra.Isomorphisms

URI: https://scilib.ai/kg/mathlib#Submodule.quotientQuotientEquivQuotientAux_mk_mk

← MathLib Explorer

English

QuotientQuotientEquivQuotientAux sends mk x to mk x.

Русский

quotientQuotientEquivQuotientAux отправляет mk x в mk x.

LaTeX

$$theorem quotientQuotientEquivQuotientAux_mk (x : M) : S.quotientQuotientEquivQuotientAux T h (Quotient.mk x) = Quotient.mk x$$

Lean4

theorem quotientQuotientEquivQuotientAux_mk_mk (x : M) :
    quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x :=
  rfl

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

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

Разделы

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

Аффилиация

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