mk — Mathlib · SciLib

English

The map mk: PerfectClosure K p → PerfectClosure K p is surjective.

Русский

Отображение mk: PerfectClosure K p → PerfectClosure K p сюръективно.

LaTeX

$$$\operatorname{Surjective}(\mathrm{mk}\;K\;p)$$$

Lean4

/-- `PerfectClosure.mk K p (n, x)` for `n : ℕ` and `x : K` is an element of `PerfectClosure K p`,
viewed as `x ^ (p ^ -n)`. Every element of `PerfectClosure K p` is of this form
(`PerfectClosure.mk_surjective`). -/
def mk (x : ℕ × K) : PerfectClosure K p :=
  Quot.mk (R K p) x

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