symm_comp

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.symm_comp

English

The composition of the inverse with the forward map equals the identity on the domain: e.symm ∘ e = id on A₁.

Русский

Обратная карта после прямой даёт тождество на домене: e.symm ∘ e = id.

LaTeX

$$$e^{\mathrm{symm}} \circ e = \mathrm{id}_{A_1}$$$

Lean4

@[simp]
theorem symm_comp (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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