symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply

Mathlib.Algebra.Ring.Equiv

URI: https://scilib.ai/kg/mathlib#RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply

← MathLib Explorer

English

For all x in R, e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x.

Русский

Для всех x в R выполняется e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x.

LaTeX

$$$$ \\forall x:\\, R,\\; e^{\\text{symm}}(e(x)) = x. $$$$

Lean4

@[simp]
theorem symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply (e : R ≃+* S) :
    ∀ x : R, e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x :=
  Equiv.symm_apply_apply e.toEquiv

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

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

Разделы

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

Аффилиация

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