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]