English
PerfectClosure(K, p) is a commutative ring extending the base ring structure with the lift of addition and multiplication via mk, mk_mul_mk, and the Frobenius action; in particular, 0 and 1 behave as expected, and distributivity holds via a liftedproof.
Русский
PerfectClosure(K, p) — коммутативное кольцо, расширяющее основанное кольцо через подъёмы сложения и умножения по mk, mk_mul_mk и действие Фробениуса; нуль и единица работают как надо, распределение — по переносам.
LaTeX
$$$\\mathrm{instCommRing}:\\; \\mathrm{PerfectClosure}(K,p)\\;\\text{is a commutative ring with lifted operations}$$$
Lean4
instance instCommRing : CommRing (PerfectClosure K p) :=
{ instAddCommGroup K p, AddMonoidWithOne.unary,
(inferInstance :
CommMonoid
(PerfectClosure K
p)) with
zero_mul := fun a => by
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
simp only [zero_add, iterate_zero, id_eq, iterate_map_zero, zero_mul, mk_zero_right]
mul_zero := fun a => by
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
simp only [iterate_zero, id_eq, iterate_map_zero, mul_zero, mk_zero_right]
left_distrib := fun e f g =>
Quot.inductionOn e fun ⟨m, x⟩ =>
Quot.inductionOn f fun ⟨n, y⟩ =>
Quot.inductionOn g fun ⟨s, z⟩ =>
by
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_comm, add_left_comm]
apply R.sound
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply, mul_add, add_comm, add_left_comm]
right_distrib := fun e f g =>
Quot.inductionOn e fun ⟨m, x⟩ =>
Quot.inductionOn f fun ⟨n, y⟩ =>
Quot.inductionOn g fun ⟨s, z⟩ =>
by
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_assoc, add_comm _ s, add_left_comm _ s]
apply R.sound
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply, add_mul, add_comm, add_left_comm] }
