hom_eq_zero_iff — Mathlib

English

For any x in Γ₀, RankOne.hom v x = 0 iff x = 0.

Русский

Для любого x ∈ Γ₀: RankOne.hom v x = 0 эквивалентно x = 0.

LaTeX

$$$\forall x:\; \mathrm{RankOne.hom}\,v\,x = 0 \iff x = 0.$$$

Lean4

/-- If `v` is a rank one valuation, then`x : Γ₀` has image `0` under `RankOne.hom v` if and
  only if `x = 0`. -/
theorem hom_eq_zero_iff {x : Γ₀} : RankOne.hom v x = 0 ↔ x = 0 :=
  ⟨fun h ↦ zero_of_hom_zero v h, fun h ↦ by rw [h, map_zero]⟩

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