toBialgHom_injective

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.toBialgHom_injective

← MathLib Explorer

English

The injection property of toEquiv is established.

Русский

Установлено свойство инъективности toEquiv.

LaTeX

$$$\\text{toEquiv\_injective}: \\forall e_1,e_2, (e_1.toEquiv = e_2.toEquiv) \\Rightarrow e_1 = e_2$$$

Lean4

theorem toBialgHom_injective : Function.Injective (toBialgHom : (A ≃ₐc[R] B) → A →ₐc[R] B) := fun _ _ H =>
  toEquiv_injective <| Equiv.ext <| BialgHom.congr_fun H

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

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

Разделы

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

Аффилиация

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