instNNRatCast — Mathlib

English

There is a canonical embedding of nonnegative rational numbers into CauSeq.Completion.Cauchy abv that respects the nonnegative rational structure.

Русский

Существует каноническое вложение неотрицательных рациональных чисел в CauSeq.Completion.Cauchy abv, сохраняющее структуру неотрицательных рациональных чисел.

LaTeX

$$$\text{instNNRatCast} : NNRatCast (CauSeq.Completion.Cauchy abv)$$$

Lean4

instance instNNRatCast : NNRatCast (Cauchy abv) where nnratCast q := ofRat q

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