mk_inv — Mathlib

English

There is an inverse operation on PerfectClosure(K,p) given by mapping mk(n,x) to mk(n,x^{-1}).

Русский

Существует операция обратного элемента на PerfectClosure(K,p), задаваемая отправлением mk(n,x) в mk(n, x^{-1}).

LaTeX

$$$\exists \mathrm{inv}: \mathrm{PerfectClosure}(K,p) \to \mathrm{PerfectClosure}(K,p)\quad\text{с}\quad \mathrm{inv}(\mathrm{mk}(K,p)(n,x))=\mathrm{mk}(K,p)(n,x^{-1}).$$$

Lean4

@[simp]
theorem mk_inv (x : ℕ × K) : (mk K p x)⁻¹ = mk K p (x.1, x.2⁻¹) :=
  rfl

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