intCast — Mathlib

English

Integers embed into PerfectClosure(K, p) via mk(K, p)(0, x) for x ∈ Z; thus (x ∈ Z) maps to (0, x) in the second coordinate.

Русский

Целые числа вкладываются в PerfectClosure(K, p) через mk(K, p)(0, x) при x ∈ ℤ; следовательно, x отображается как (0, x).

LaTeX

$$$(x : \\mathbb{Z}) : (x : PerfectClosure K p) = mk K p (0, x)$$$

Lean4

theorem intCast (x : ℤ) : (x : PerfectClosure K p) = mk K p (0, x) := by cases x <;> simp [natCast K p 0]

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