instStarModuleNNRealReal

Mathlib.Data.NNReal.Star

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

English

The NNReal module over Real is a star module with a trivial star action.

Русский

Модуль NNReal над Real имеет тривиальное звездочное действие.

LaTeX

$$$ \text{ NNReal is a StarModule over Real with trivial star. }$$$

Lean4

instance : StarModule ℝ≥0 ℝ where star_smul := by simp only [star_trivial, forall_const]

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

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

Разделы

Аффилиация

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