leftInverse_symm

Mathlib.Algebra.Star.StarRingHom

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

English

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

Русский

Левый обратный элемент к symm есть у e; e.symm является левым обратным к e.

LaTeX

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

Lean4

theorem leftInverse_symm (e : A ≃⋆+* B) : Function.LeftInverse e.symm e :=
  e.left_inv

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

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

Разделы

Аффилиация

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