mul_left_inj

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.mul_left_inj

English

For c ≠ 0 and c ≠ ∞, a·c = b·c ⇔ a = b.

Русский

Для c ≠ 0 и c ≠ ∞ верно a·c = b·c ⇔ a = b.

LaTeX

$$$c \neq 0 \land c \neq \infty \Rightarrow a c = b c \iff a = b$$$

Lean4

protected theorem mul_left_inj (h0 : c ≠ 0) (hinf : c ≠ ∞) : a * c = b * c ↔ a = b :=
  mul_comm c a ▸ mul_comm c b ▸ ENNReal.mul_right_inj h0 hinf

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

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

Разделы

Аффилиация

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