instMulArchimedeanNNRat

Mathlib.Algebra.Order.Archimedean.Basic

URI: https://scilib.ai/kg/mathlib#instMulArchimedeanNNRat

English

MulArchimedean structure lifts to the nonnegative rationals: MulArchimedean NN Rat.

Русский

Структура MulArchimedean передается на неотрицательные рациональные числа: MulArchimedean NN Rat.

LaTeX

$$$$ \text{MulArchimedean NN Rat}. $$$$

Lean4

instance : MulArchimedean NNRat :=
  Nonneg.instMulArchimedean

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

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

Разделы

Аффилиация

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