English
Natural numbers embed into PerfectClosure(K, p) by mk(K, p) with the first component equal to the natural number and the second equal to the natural itself; hence (n, x) maps to the element representing n in the first coordinate and x in the second under natCast.
Русский
Натуральные числа инкрустируются в PerfectClosure(K, p) через mk(K, p) с первой координатой n и второй координатой x, так что x как элемент K вставляется во вторую часть.
LaTeX
$$$\\forall n,x:\\mathbb{N},\\; (x:PerfectClosure K p) = mk K p (n, x) $$$
Lean4
theorem natCast (n x : ℕ) : (x : PerfectClosure K p) = mk K p (n, x) := by
induction n with
| zero =>
induction x with
| zero => simp
| succ x ih => simp [Nat.cast_succ, ih, one_def]
| succ n ih =>
rw [ih]; apply Quot.sound
suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by rwa [frobenius_natCast K p x] at this
apply R.intro
