one_power

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.one_power

English

The cardinal of 1 to the power a equals 1: 1^{a} = 1.

Русский

Кардинал единицы в любую степень равен единице: 1^{a} = 1.

LaTeX

$$$1^{a} = 1$$$

Lean4

@[simp]
theorem one_power {a : Cardinal} : (1 : Cardinal) ^ a = 1 :=
  inductionOn a fun _ => mk_eq_one _

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

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

Разделы

Аффилиация

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