instCommMonoid — Mathlib

English

The multiplicative identity in PerfectClosure(K, p) is the class of (0, 1): 1 = mk(K, p, (0, 1)).

Русский

Единица в PerfectClosure(K, p) равна классy mk(K, p, (0, 1)).

LaTeX

$$$1 = mk\\,K\\,p\\big(0,1\\big)$$$

Lean4

instance instCommMonoid : CommMonoid (PerfectClosure K p) :=
  {
    (inferInstance :
      Mul
        (PerfectClosure K
          p)) with
    mul_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 [mul_assoc, iterate_map_mul, ← iterate_add_apply, add_comm, add_left_comm]
    one := mk K p (0, 1)
    one_mul := fun e =>
      Quot.inductionOn e fun ⟨n, x⟩ =>
        congr_arg (Quot.mk _) <| by simp only [iterate_map_one, iterate_zero_apply, one_mul, zero_add]
    mul_one := fun e =>
      Quot.inductionOn e fun ⟨n, x⟩ =>
        congr_arg (Quot.mk _) <| by simp only [iterate_map_one, iterate_zero_apply, mul_one, add_zero]
    mul_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, mul_comm] }

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