instSMulNNRat

Mathlib.Algebra.Field.Subfield.Defs

URI: https://scilib.ai/kg/mathlib#SubfieldClass.instSMulNNRat

Lean4

instance instSMulNNRat (s : S) : SMul ℚ≥0 s where smul q x := ⟨q • x, nnqsmul_mem s q x.2⟩

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

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

Разделы

Аффилиация

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