pow_snd — Mathlib

English

Let p = (a,b) ∈ α × β and c ∈ E. Then p^c = (a^c, b^c). In particular, the second coordinate satisfies (p^c).2 = b^c.

Русский

Пусть p = (a,b) ∈ α × β и c ∈ E. Тогда p^c = (a^c, b^c). В частности, вторая координата удовлетворяет (p^c)₂ = b^c.

LaTeX

$$$ (a,b)^c = (a^c, b^c) $$$

Lean4

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

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