add_one_nmul

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

(a + 1) ⊗ b = a ⊗ b ⊞ b.

Русский

(a + 1) ⊗ b = a ⊗ b ⊞ b.

LaTeX

$$$(a + 1) \otimes b = a \otimes b \boxplus b$$$

Lean4

theorem add_one_nmul : ∀ a b, (a + 1) ⨳ b = a ⨳ b ♯ b :=
  succ_nmul

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

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

Разделы

Аффилиация

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