prod_mono_right

Mathlib.Algebra.Ring.Subring.Basic

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

English

Monotone in the second argument: s.prod t is monotone in t.

Русский

Монотонно по второй переменной: s.prod t монотонно по t.

LaTeX

$$$ \forall t_1 \le t_2, \ s .prod t_1 \le s .prod t_2 $$$

Lean4

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

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

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

Разделы

Аффилиация

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