English
Let Γ₀ be a type with a linear ordered commutative monoid with zero, and v a valuation R Γ₀ compatible. Then IsNontrivial R is equivalent to v.IsNontrivial.
Русский
Пусть Γ₀ имеет линейный упорядоченный коммутативный моноид с нулём, и v — валюация. Тогда IsNontrivial R эквивалентно v.IsNontrivial.
LaTeX
$$$\\text{IsNontrivial }R \\;\\iff\\; v.IsNontrivial$$$
Lean4
theorem isNontrivial_iff_isNontrivial {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
[v.Compatible] : IsNontrivial R ↔ v.IsNontrivial :=
by
constructor
· rintro ⟨r, hr, hr'⟩
induction r using ValueGroupWithZero.ind with
| mk r s
have hγ : v r ≠ 0 := by simpa [Valuation.Compatible.rel_iff_le (v := v)] using hr
have hγ' : v r ≤ v s → v r < v s := by simpa [Valuation.Compatible.rel_iff_le (v := v)] using hr'
by_cases hr : v r = 1
· exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩
· exact ⟨r, by simpa using hγ, hr⟩
· rintro ⟨r, hr, hr'⟩
exact
⟨valuation R r, (isEquiv v (valuation R)).ne_zero.mp hr, by
simpa [(isEquiv v (valuation R)).eq_one_iff_eq_one] using hr'⟩
