mk_le_mk_smul

Mathlib.Algebra.Order.Module.Archimedean

URI: https://scilib.ai/kg/mathlib#ArchimedeanClass.mk_le_mk_smul

English

A gcongr variant asserting the same monotonicity as algebraMap_mono in a gcongr setting.

Русский

Вариант gcongr, эквивалентный монотонности algebraMap_mono в настройке gcongr.

LaTeX

$$$a_1 \le a_2 \Rightarrow \text{algebraMap } a_1 \le \text{algebraMap } a_2$$$

Lean4

theorem mk_le_mk_smul (a : M) (k : K) : mk a ≤ mk (k • a) := by obtain rfl | h := eq_or_ne k 0 <;> simp [*]

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

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

Разделы

Аффилиация

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