instRing — Mathlib

English

The ring structure on WithVal v is inherited from R; WithVal v is a ring whose operations are those of R under the natural identification.

Русский

Кольцевая структура для WithVal v получается от R; WithVal v — кольцо, операции которого совпадают с операциями R через естественное соответствие.

LaTeX

$$$WithVal(v)$ is a ring$$

Lean4

instance [Ring R] (v : Valuation R Γ₀) : Ring (WithVal v) :=
  inferInstanceAs (Ring R)

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