injective_pointReflection_left_of_module

English

If 2 is invertible in the ring, then for every y, the map x ↦ pointReflection k x y is injective.

Русский

Если 2 обращаемо в кольце, то для каждого y отображение x ↦ pointReflection k x y инъективно.

LaTeX

$$[Invertible(2:k)] ∀ y, Injective (x ↦ pointReflection k x y)$$

Lean4

theorem injective_pointReflection_left_of_module [Invertible (2 : k)] :
    ∀ y, Injective fun x : P₁ => pointReflection k x y :=
  injective_pointReflection_left_of_injective_two_nsmul k fun x y h =>
    by
    dsimp at h
    rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y, (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

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