lineMap_same_apply

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.lineMap_same_apply

English

The line map is injective on the scalar parameter whenever the two endpoints are distinct.

Русский

Линейная карта инъективна по скаляру, если концы различны.

LaTeX

$$$\text{lineMap}_{p_0,p_1}: k \to P_1$ is injective whenever \ p_0 \neq p_1$.$$

Lean4

theorem lineMap_same_apply (p : P1) (c : k) : lineMap p p c = p := by simp [lineMap_apply]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru