eq_trivialRel_of_compatible_one — Mathlib

English

The trivial relation equals ValuativeRel.ofValuation(1).

Русский

Тривиальное отношение равно ValuativeRel.ofValuation(1).

LaTeX

$$$\\mathrm{trivialRel} = \\mathrm{ValuativeRel.ofValuation}(1)$$$

Lean4

theorem eq_trivialRel_of_compatible_one [h : ValuativeRel R] [hv : Valuation.Compatible (1 : Valuation R Γ)] :
    h = trivialRel := by
  ext
  change _ ↔ if _ = 0 then _ else _
  rw [hv.rel_iff_le]
  split_ifs <;> simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

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