lineMap_injective — Mathlib

English

Injectivity of lineMap follows from distinct endpoints when NoZeroSmulDivisors holds.

Русский

Инъективность lineMap следует из различности концов при NoZeroSmulDivisors.

LaTeX

$$$\text{NoZeroSmulDivisors}(k,V_1) \; \Rightarrow\; \text{Injective}(\text{lineMap }p_0 p_1) $$$

Lean4

theorem lineMap_injective [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} (h : p₀ ≠ p₁) :
    Function.Injective (lineMap p₀ p₁ : k → P1) := fun _c₁ _c₂ hc => (lineMap_eq_lineMap_iff.mp hc).resolve_left h

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