rel_mul_left

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.rel_mul_left

English

Multiplication on the left preserves the relation: if x ≤ᵥ y then z·x ≤ᵥ z·y.

Русский

Умножение слева сохраняет отношение: если x ≤ᵥ y, то z·x ≤ᵥ z·y.

LaTeX

$$$ {x y : R} (z) : x \le\!_v y \rightarrow (z \cdot x) \le\!_v (z \cdot y). $$$

Lean4

theorem rel_mul_left {x y : R} (z) : x ≤ᵥ y → (z * x) ≤ᵥ (z * y) :=
  by
  rw [mul_comm z x, mul_comm z y]
  apply rel_mul_right

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

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

Разделы

Аффилиация

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