mul_eq_mul_left_iff

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0 := by
  by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]

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

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

Разделы

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

Аффилиация

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