left_cancel_posSubmonoid

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

← MathLib Explorer

English

Left cancellation by a posSubmonoid element: u·x ≤ᵥ u·y iff x ≤ᵥ y.

Русский

Левое отменение элементом posSubmonoid: u·x ≤ᵥ u·y ⇔ x ≤ᵥ y.

LaTeX

$$$ u * x \le\!_v u * y \;\Leftrightarrow\; x \le\!_v y $$$

Lean4

@[simp]
theorem left_cancel_posSubmonoid (x y : R) (u : posSubmonoid R) : u * x ≤ᵥ u * y ↔ x ≤ᵥ y := by
  simp only [← right_cancel_posSubmonoid x y u, mul_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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