English
WithAbs is a type family assigning to each AbsoluteValue v on R a copy of R.
Русский
WithAbs — это семейство типов, сопоставляющее каждому абсолютному значению v на R копию кольца R.
LaTeX
$$WithAbs(v) \\cong R$$
Lean4
/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
on a semiring that depend on absolute values.
This is also helpful when dealing with several absolute values on the same semiring. -/
@[nolint unusedArguments]
def WithAbs [Semiring R] : AbsoluteValue R S → Type _ := fun _ => R
