two_add_one_eq_three

Mathlib.Data.Nat.Cast.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$2 + 1 = 3$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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