one_add_one_eq_two

Mathlib.Data.Nat.Cast.Defs

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

English

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

Русский

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

LaTeX

$$$1 + 1 = (2 : R)$$$

Lean4

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

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

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

Разделы

Аффилиация

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