instRatCast

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.instRatCast

English

There is a canonical embedding of rational numbers into CauSeq.Completion.Cauchy abv that is compatible with the Cauchy construction.

Русский

Существуют рациональные числа внутри CauSeq.Completion.Cauchy abv, согласованные с конструкцией Коши.

LaTeX

$$$\text{instRatCast} : RatCast (CauSeq.Completion.Cauchy abv)$$$

Lean4

instance instRatCast : RatCast (Cauchy abv) where ratCast q := ofRat q

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru