pow_fst

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.pow_fst

English

The first coordinate under powers matches: (p^c).fst = p.fst^c.

Русский

Первая координата при возведении в степень совпадает: (p^c).fst = p.fst^c.

LaTeX

$$(p^c)_1 = p_1^c$$

Lean4

@[to_additive existing (attr := simp) (reorder := 6 7) smul_fst]
theorem pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c :=
  rfl

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

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

Разделы

Аффилиация

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