zero_srel_mul

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

← MathLib Explorer

English

If 0 <ᵥ x and 0 <ᵥ y then 0 <ᵥ x·y.

Русский

Если 0 <ᵥ x и 0 <ᵥ y, то 0 <ᵥ x·y.

LaTeX

$$$ {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y$$$

Lean4

theorem zero_srel_mul {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y :=
  by
  contrapose! hy
  rw [not_srel_iff] at hy ⊢
  rw [show (0 : R) = x * 0 by simp, mul_comm x y, mul_comm x 0] at hy
  exact rel_mul_cancel hx hy

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

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

Разделы

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

Аффилиация

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