mul_sub

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

a · (b − c) = a · b − a · c.

Русский

a · (b − c) = a · b − a · c.

LaTeX

$$$a \\\\cdot (b - c) = a \\\\cdot b - a \\\\cdot c$$$

Lean4

theorem mul_sub (a b c : Ordinal) : a * (b - c) = a * b - a * c :=
  if a0 : a = 0 then by simp only [a0, zero_mul, sub_self]
  else eq_of_forall_ge_iff fun d => by rw [sub_le, ← le_div a0, sub_le, ← le_div a0, mul_add_div _ a0]

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

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

Разделы

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

Аффилиация

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