verschiebung_injective — Mathlib

English

The Verschiebung map is injective: if verschiebung(x) = verschiebung(y), then x = y.

Русский

Отображение Verschiebung инъективно: если Verschiebung(x) = Verschiebung(y), то x = y.

LaTeX

$$$$ (\\\\forall x,y:\\\\; 𝕎R), \\\\text{verschiebung}(x) = \\\\text{verschiebung}(y) \Rightarrow x = y. $$$$

Lean4

theorem verschiebung_injective : Function.Injective (verschiebung : 𝕎 R → 𝕎 R) :=
  by
  rw [injective_iff_map_eq_zero]
  intro w h
  ext n
  rw [← verschiebung_coeff_succ, h]
  simp only [zero_coeff]

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