coe_mul — Mathlib

English

The function part of the product of two affine isometry equivalences is the composition of their underlying functions.

Русский

Часть функции произведения двух аффинных изометрий равна композиции соответствующих отображений.

LaTeX

$$$\mathrm{toFun}(e * e') = \mathrm{toFun}(e) \circ \mathrm{toFun}(e')$$$

Lean4

@[simp]
theorem coe_mul (e e' : P ≃ᵃⁱ[𝕜] P) : ⇑(e * e') = e ∘ e' :=
  rfl

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