trans — Mathlib

English

The underlying function of the composition of two affine equivalences equals the composition of their underlying functions.

Русский

Базовая функция композиции двух аффинных эквивалентностей равна композиции их базовых функций.

LaTeX

$$$\operatorname{toFun}(e\,\mathrm{trans}\, e') = (\operatorname{toFun}(e'))\circ (\operatorname{toFun}(e))$$$

Lean4

/-- Composition of two `AffineEquiv`alences, applied left to right. -/
@[trans]
def trans (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : P₁ ≃ᵃ[k] P₃
    where
  toEquiv := e.toEquiv.trans e'.toEquiv
  linear := e.linear.trans e'.linear
  map_vadd' p v := by simp only [LinearEquiv.trans_apply, coe_toEquiv, (· ∘ ·), Equiv.coe_trans, map_vadd]

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