English
If ValuativeRel is defined and 1 is compatible, then the valuative relation is trivial.
Русский
Если задана валюативная связь и 1 совместим, то валюативное отношение тривиально.
LaTeX
$$$h = \\mathrm{trivialRel}$ under $hv: \\mathrm{Valuation.Compatible}(1)$$$
Lean4
/-- The trivial valuative relation on a domain `R`, such that all non-zero elements are related.
The domain condition is necessary so that the relation is closed when multiplying.
-/
def trivialRel : ValuativeRel R where
rel x y := if y = 0 then x = 0 else True
rel_total _ _ := by split_ifs <;> simp_all
rel_trans _ _ := by split_ifs; simp_all
rel_add _ _ := by split_ifs; simp_all
rel_mul_right _ := by split_ifs <;> simp_all
rel_mul_cancel _ := by split_ifs <;> simp_all
not_rel_one_zero := by split_ifs <;> simp_all
