three_add_one_eq_four

Mathlib.Data.Nat.Cast.Defs

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

← MathLib Explorer

English

In any AddMonoidWithOne R, 3 + 1 = 4 in R.

Русский

В любом AddMonoidWithOne R, 3 + 1 = 4 в R.

LaTeX

$$$3 + 1 = 4$$$

Lean4

theorem three_add_one_eq_four [AddMonoidWithOne R] : 3 + 1 = (4 : R) :=
  by
  rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
  apply congrArg
  decide

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

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

Разделы

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

Аффилиация

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