subsingleton_units_valueGroupWithZero_of_trivialRel

English

From a trivial Rel, it follows that R is not nontrivial.

Русский

Из тривиального отношения следует, что R не является ненулевым.

LaTeX

$$$\\neg \\mathrm{IsNontrivial}(R)$$$

Lean4

theorem subsingleton_units_valueGroupWithZero_of_trivialRel [ValuativeRel R]
    [Valuation.Compatible (1 : Valuation R Γ)] : Subsingleton (ValueGroupWithZero R)ˣ :=
  by
  constructor
  intro a b
  have : (valuation R).IsEquiv (1 : Valuation R Γ) := isEquiv _ _
  obtain ⟨r, s, hr⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq a
  obtain ⟨t, u, ht⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq b
  rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.val_eq] <;> simp [one_apply_posSubmonoid]

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