mul_eq_mul_right_iff

Mathlib.Algebra.GroupWithZero.Basic

URI: https://scilib.ai/kg/mathlib#mul_eq_mul_right_iff

← MathLib Explorer

English

In a CancelMonoidWithZero, a c = b c iff a = b or c = 0.

Русский

В CancelMonoidWithZero, a c = b c эквивалентно a = b или c = 0.

LaTeX

$$$$ a \cdot c = b \cdot c \iff a = b \lor c = 0 $$$$

Lean4

@[simp]
theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 := by
  by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]

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

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

Разделы

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

Аффилиация

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