isNontrivial_iff_nontrivial_units

English

IsNontrivial R is equivalent to the nontriviality of the units of ValueGroupWithZero R.

Русский

IsNontrivial R эквивалентно неtrivialности группы единиц ValueGroupWithZero R.

LaTeX

$$$\\operatorname{IsNontrivial}(R) \\;\\iff\\; (\\mathrm{ValueGroupWithZero}(R))^{\\times} \\text{ is nontrivial}$$$

Lean4

theorem isNontrivial_iff_nontrivial_units : IsNontrivial R ↔ Nontrivial (ValueGroupWithZero R)ˣ :=
  by
  constructor
  · rintro ⟨γ, hγ, hγ'⟩
    refine ⟨Units.mk0 _ hγ, 1, ?_⟩
    simp [← Units.val_eq_one, hγ']
  · rintro ⟨r, s, h⟩
    rcases eq_or_ne r 1 with rfl | hr
    · exact ⟨s.val, by simp, by simpa using h.symm⟩
    · exact ⟨r.val, by simp, by simpa using hr⟩

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