English
Every field K carries a GrindField structure compatible with exponentiation, i.e., z-powers coincide with ordinary powers.
Русский
Каждое поле K обладает структурой GrindField, совместимой с возведением в степень, то есть z-переходы совпадают с обычными степенями.
LaTeX
$$$\\text{GrindField}(K) \\text{ with } z^{n}(a) = a^{n}$$$
Lean4
instance (priority := 100) toGrindField [Field K] : Lean.Grind.Field K :=
{ CommRing.toGrindCommRing K, ‹Field K› with
zpow := ⟨fun a n => a ^ n⟩
zpow_zero a := by simp
zpow_succ a
n := by
by_cases h : a = 0
· rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
· rw [zpow_add_one₀ h]
zpow_neg a n := by simp
zero_ne_one := zero_ne_one' K }
