instFunLike

Mathlib.RingTheory.DividedPowers.DPMorphism

URI: https://scilib.ai/kg/mathlib#DividedPowers.DPMorphism.instFunLike

Lean4

instance instFunLike : FunLike (DPMorphism hI hJ) A B
    where
  coe h := h.toRingHom
  coe_injective' h h'
    hh' := by
    cases h; cases h'; congr
    dsimp at hh'; ext; rw [hh']

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

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

Разделы

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

Аффилиация

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