rightInverse_symm

Mathlib.Algebra.Star.StarRingHom

URI: https://scilib.ai/kg/mathlib#StarRingEquiv.rightInverse_symm

English

The right inverse of symm is e itself, i.e., e.symm is a right inverse of e.

Русский

Правое обратное у symm — это само e; e.symm является правым обратным к e.

LaTeX

$$$\\text{RightInverse}(\\text{coeff}(e^{-1}), \\text{coeff}(e))$$$

Lean4

theorem rightInverse_symm (e : A ≃⋆+* B) : Function.RightInverse e.symm e :=
  e.right_inv

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

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

Разделы

Аффилиация

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