English
IsRankLeOne R holds if and only if MulArchimedean (ValueGroupWithZero R) holds.
Русский
IsRankLeOne R выполняется тогда и только если MulArchimedean (ValueGroupWithZero R) выполняется.
LaTeX
$$$\mathrm{IsRankLeOne\}R \iff \mathrm{MulArchimedean}(\mathrm{ValueGroupWithZero}\,R)$$$
Lean4
theorem isRankLeOne_iff_mulArchimedean : IsRankLeOne R ↔ MulArchimedean (ValueGroupWithZero R) :=
by
constructor
· rintro ⟨⟨f, hf⟩⟩
exact .comap f.toMonoidHom hf
· intro h
by_cases H : IsNontrivial R
· rw [isNontrivial_iff_isNontrivial (valuation R)] at H
rw [← (valuation R).nonempty_rankOne_iff_mulArchimedean] at h
obtain ⟨f⟩ := h
exact isRankLeOne_of_rankOne
· refine ⟨⟨{ emb := 1, strictMono := ?_ }⟩⟩
intro a b
contrapose! H
obtain ⟨H, H'⟩ := H
rcases eq_or_ne a 0 with rfl | ha
· simp_all
rcases eq_or_ne a 1 with rfl | ha'
· exact ⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩
· exact ⟨⟨a, ha, ha'⟩⟩
