repr_opow

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#NONote.repr_opow

English

repr(opow a b) = repr(a) ^ repr(b).

Русский

repr(opow a b) = repr(a) ^ repr(b).

LaTeX

$$$$ \operatorname{repr}(\mathrm{opow}\ a\ b) = \operatorname{repr}(a)^{\operatorname{repr}(b)}. $$$$

Lean4

theorem repr_opow (a b) : repr (opow a b) = repr a ^ repr b :=
  ONote.repr_opow a.1 b.1

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

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

Разделы

Аффилиация

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