instIsNontrivial — Mathlib

English

Under the same rank-one discrete assumption, the valuation v is nontrivial.

Русский

При тех же предпосылках валидация v не является тривиальной.

LaTeX

$$$v\,\text{IsNontrivial}$$$

Lean4

instance [IsRankOneDiscrete v] : v.IsNontrivial := by
  constructor
  obtain ⟨⟨γ, π, hπ⟩, hγ⟩ := (nontrivial_iff_exists_ne (1 : valueMonoid v)).mp (by infer_instance)
  use π
  constructor
  · simp [hπ]
  · rw [hπ]
    simp only [← MonoidWithZeroHom.coe_one, ne_eq, Subtype.mk.injEq] at hγ
    simp [hγ, Units.val_eq_one]

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