coe_mul

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.coe_mul

English

The coercion of the product equals composition: ⇑(f * g) = f ∘ g.

Русский

Коэрцирование произведения равно композиции: ⇑(f*g) = f ∘ g.

LaTeX

$$$\\forall f,g \\in CircleDeg1Lift,\\ \\text{coe}(f*g) = \\text{coe}(f) \\circ \\text{coe}(g)$$$

Lean4

@[simp]
theorem coe_mul : ⇑(f * g) = f ∘ g :=
  rfl

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

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

Разделы

Аффилиация

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