zero_of_hom_zero — Mathlib

English

If the rank-one homomorphism maps x to 0, then x is 0.

Русский

Если образ x под гомоморфизм RankOne равен 0, то x = 0.

LaTeX

$$$\forall x:\; \mathrm{hom}\,v(x) = 0 \Rightarrow x = 0.$$$

Lean4

/-- If `v` is a rank one valuation and `x : Γ₀` has image `0` under `RankOne.hom v`, then
  `x = 0`. -/
theorem zero_of_hom_zero {x : Γ₀} (hx : hom v x = 0) : x = 0 :=
  by
  refine (eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm
  have hs := strictMono v h_lt
  rw [map_zero, hx] at hs
  exact hs.false

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