mul_tsub

Mathlib.Algebra.Order.Ring.Canonical

URI: https://scilib.ai/kg/mathlib#AddLECancellable.mul_tsub

← MathLib Explorer

English

0 < a^2 iff a ≠ 0.

Русский

0 < a^2 эквивалентно a ≠ 0.

LaTeX

$$$0 < a^2 \iff a \neq 0$$$

Lean4

protected theorem mul_tsub {a b c : R} (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c :=
  by
  obtain (hbc | hcb) := total_of (· ≤ ·) b c
  · rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]
  · apply h.eq_tsub_of_add_eq
    rw [← mul_add, tsub_add_cancel_of_le hcb]

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

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

Разделы

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

Аффилиация

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