rotation_trans — Mathlib

English

The composition of two rotations corresponds to the rotation by the product: rotation(a) trans rotation(b) = rotation(b a).

Русский

Сопоставление двух вращений соответствует вращению на произведение: rotation(a) trans rotation(b) = rotation(b a).

LaTeX

$$$(rotation\;a).trans(rotation\;b) = rotation\; (b \cdot a)$$$

Lean4

@[simp]
theorem rotation_trans (a b : Circle) : (rotation a).trans (rotation b) = rotation (b * a) :=
  by
  ext1
  simp

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