instAddCommGroup — Mathlib

English

PerfectClosure(K, p) is an additive commutative group: addition, zero, negation, and additive inverses are defined by quotient-wise lifts of the corresponding operations on N × K with Frobenius actions.

Русский

PerfectClosure(K, p) является аддитивной перестановной группой: сложение, нуль, отрицание и аддитивные противоположные определены по подъемам через эквивалентность на N × K с действиями Фробениуса.

LaTeX

$$$\\text{instAddCommGroup}:\\; (\\PerfectClosure\\ K\\ p) \\\\rightarrow\\text{AddCommGroup}$$$

Lean4

instance instAddCommGroup : AddCommGroup (PerfectClosure K p) :=
  { (inferInstance : Add (PerfectClosure K p)),
    (inferInstance :
      Neg
        (PerfectClosure K
          p)) with
    add_assoc := fun e f g =>
      Quot.inductionOn e fun ⟨m, x⟩ =>
        Quot.inductionOn f fun ⟨n, y⟩ =>
          Quot.inductionOn g fun ⟨s, z⟩ => by
            apply congr_arg (Quot.mk _)
            simp only [iterate_map_add, ← iterate_add_apply, add_assoc, add_comm s _]
    zero := 0
    zero_add := fun e =>
      Quot.inductionOn e fun ⟨n, x⟩ =>
        congr_arg (Quot.mk _) <| by simp only [iterate_map_zero, iterate_zero_apply, zero_add]
    add_zero := fun e =>
      Quot.inductionOn e fun ⟨n, x⟩ =>
        congr_arg (Quot.mk _) <| by simp only [iterate_map_zero, iterate_zero_apply, add_zero]
    sub_eq_add_neg := fun _ _ => rfl
    neg_add_cancel := fun e =>
      Quot.inductionOn e fun ⟨n, x⟩ => by
        simp only [quot_mk_eq_mk, neg_mk, mk_add_mk, iterate_map_neg, neg_add_cancel, mk_zero_right]
    add_comm := fun e f =>
      Quot.inductionOn e fun ⟨m, x⟩ => Quot.inductionOn f fun ⟨n, y⟩ => congr_arg (Quot.mk _) <| by simp only [add_comm]
    nsmul := nsmulRec
    zsmul := zsmulRec }

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