coe_trans_to_affineMap — Mathlib

English

The affine map underlying e.trans e' equals the composition of the affine maps underlying e' and e.

Русский

Базовая аффинная карта e.trans e' равна композиции базовых карт e' и e.

LaTeX

$$$ (e.trans e').toAffineMap = (e'.toAffineMap)\circ (e.toAffineMap) $$$

Lean4

@[simp]
theorem coe_trans_to_affineMap (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
    (e.trans e' : P₁ →ᵃ[k] P₃) = (e' : P₂ →ᵃ[k] P₃).comp e :=
  rfl

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