natCast_eq_iff — Mathlib

English

Equality (x : PerfectClosure K p) = y, with x,y ∈ ℕ, is equivalent to equality (x : K) = y in the base ring; the equivalence is decided by natCast and the structure mk.

Русский

Равенство (x : PerfectClosure K p) = y для x,y ∈ ℕ эквивалентно равенству (x : K) = y в основании; эквивалентность определяется natCast и структурой mk.

LaTeX

$$$(x : PerfectClosure K p) = y \\;\\text{ iff }\\; (x : K) = y$$$

Lean4

theorem natCast_eq_iff (x y : ℕ) : (x : PerfectClosure K p) = y ↔ (x : K) = y :=
  by
  constructor <;> intro H
  · rw [natCast K p 0, natCast K p 0, mk_eq_iff] at H
    obtain ⟨z, H⟩ := H
    simpa only [zero_add, iterate_fixed (frobenius_natCast K p _)] using H
  rw [natCast K p 0, natCast K p 0, H]

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