mul_right_not_lt

Mathlib.Algebra.EuclideanDomain.Defs

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.mul_right_not_lt

English

If a ≠ 0 in a Euclidean domain, then a·b is not strictly smaller than b in the Euclidean order.

Русский

Если a ≠ 0 в евклидовом кольце, то a·b не является меньшим по отношению к b.

LaTeX

$$$$ a \\neq 0 \\Rightarrow \\neg (a \\cdot b \\prec b). $$$$

Lean4

theorem mul_right_not_lt {a : R} (b) (h : a ≠ 0) : ¬a * b ≺ b :=
  by
  rw [mul_comm]
  exact mul_left_not_lt b h

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

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

Разделы

Аффилиация

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