smoothRightMul_one

Mathlib.Geometry.Manifold.Algebra.Monoid

URI: https://scilib.ai/kg/mathlib#smoothRightMul_one

English

Right multiplication by the unit element is the identity: R_one = id.

Русский

Правое умножение на единицу является тождественным отображением: R_1 = id.

LaTeX

$$$R(1) = \mathrm{id}$$$

Lean4

theorem smoothRightMul_one : (𝑹 I g') 1 = g' :=
  one_mul g'

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

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

Разделы

Аффилиация

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