mul_eq_mul_left

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.mul_eq_mul_left

English

If a ≠ 0 in NNReal, then a*b = a*c iff b=c.

Русский

Если a ≠ 0 в ℝ≥0, то a·b = a·c эквивалентно b=c.

LaTeX

$$$$ a \neq 0 \implies a b = a c \iff b = c. $$$$

Lean4

theorem mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) : a * b = a * c ↔ b = c := by rw [mul_eq_mul_left_iff, or_iff_left h]

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

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

Разделы

Аффилиация

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