mul_div_cancel_left₀

Mathlib.Algebra.GroupWithZero.Defs

URI: https://scilib.ai/kg/mathlib#mul_div_cancel_left₀

English

Similarly, for any b ≠ 0, (a·b)/a = b.

Русский

Аналогично, для любого a ≠ 0: (a·b)/a = b.

LaTeX

$$$\forall b,\ a \neq 0 \Rightarrow (a \cdot b)/a = b$$$

Lean4

@[simp]
theorem mul_div_cancel_left₀ (b : M₀) {a : M₀} (ha : a ≠ 0) : a * b / a = b := by
  rw [mul_comm, mul_div_cancel_right₀ _ ha]

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

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

Разделы

Аффилиация

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