English
LineMap composed with another lineMap yields a single line along the same base that scales by the product of parameters: lineMap(p0, lineMap(p0, p1, c), d) = lineMap(p0, p1, d c).
Русский
Линейная карта, применённая к результирующей точке второй карты, даёт линию с параметром, равным произведению параметров: lineMap(p0, lineMap(p0,p1,c), d) = lineMap(p0,p1, d c).
LaTeX
$$$ lineMap(p_0, lineMap(p_0,p_1,c), d) = lineMap(p_0,p_1, d \\cdot c) $$$
Lean4
@[simp]
theorem lineMap_lineMap_right (p₀ p₁ : P1) (c d : k) : lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c) := by
simp [lineMap_apply, mul_smul]