mul_right_inj

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.mul_right_inj

← MathLib Explorer

English

If a > 0, then a·b = a·c implies b = c.

Русский

Если a > 0, то a·b = a·c означает b = c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ a > 0 \rightarrow (a\cdot b = a\cdot c \iff b = c)$$$

Lean4

@[deprecated mul_left_cancel_iff_of_pos (since := "2025-08-26")]
theorem mul_right_inj {a b c : Ordinal} (a0 : 0 < a) : a * b = a * c ↔ b = c :=
  mul_left_cancel_iff_of_pos a0

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

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

Разделы

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

Аффилиация

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