mk_succ_pow — Mathlib

English

Within PerfectClosure, increasing the first component by 1 corresponds to taking p-th power in the second component.

Русский

В PerfectClosure при увеличении первого компонента на 1 соответствующее выражение во втором компоненте поднимается в степень p.

LaTeX

$$$\mathrm{mk}\;K\;p\;\langle m+1, x^p\rangle = \mathrm{mk}\;K\;p\;\langle m, x\rangle$$$

Lean4

@[simp]
theorem mk_succ_pow (m : ℕ) (x : K) : mk K p ⟨m + 1, x ^ p⟩ = mk K p ⟨m, x⟩ :=
  Eq.symm <| Quot.sound (R.intro m x)

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