English
Let R be a commutative ring equipped with a valuative relation. For any predicate M on the value group with zero, if M holds for every representative mk(x, y), then M holds for every element of ValueGroupWithZero R.
Русский
Пусть R — коммутативное кольцо с валюативным отношением. Для любой предикатной функции M на ValueGroupWithZero R, если M верно для каждого представителя mk(x, y), то M верно для каждого элемента ValueGroupWithZero R.
LaTeX
$$$ \forall R [\text{CommRing } R] [\text{ValuativeRel } R], \forall M:\operatorname{ValueGroupWithZero} R \to \mathsf{Prop},\,\biggl(\forall x,y \in R, M(\operatorname{ValueGroupWithZero.mk} x y)\biggr) \Rightarrow \forall t:\operatorname{ValueGroupWithZero} R, M(t)$$$
Lean4
protected theorem ind {motive : ValueGroupWithZero R → Prop} (mk : ∀ x y, motive (.mk x y)) (t : ValueGroupWithZero R) :
motive t :=
Quotient.ind (fun (x, y) => mk x y) t
