prod_mono_right

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalSubsemiring.prod_mono_right

English

For fixed s, the map t ↦ s.prod t is monotone.

Русский

Для фиксированного s отображение t ↦ s.prod t монотонно.

LaTeX

$$Monotone fun t => s.prod t$$

Lean4

theorem prod_mono_right (s : NonUnitalSubsemiring R) : Monotone fun t : NonUnitalSubsemiring S => s.prod t :=
  prod_mono (le_refl s)

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

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

Разделы

Аффилиация

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