instCommRingOfCommMonoid — Mathlib

Lean4
instance [CommMonoid α] : CommRing (FreeAbelianGroup α) :=
  { FreeAbelianGroup.ring α with
    mul_comm := fun x y ↦ by
      refine FreeAbelianGroup.induction_on x (zero_mul y) ?_ ?_ ?_
      · intro s
        refine FreeAbelianGroup.induction_on y (zero_mul _).symm ?_ ?_ ?_
        · intro t
          dsimp only [(· * ·), Mul.mul]
          iterate 4 rw [lift_apply_of]
          congr 1
          exact mul_comm _ _
        · intro t ih
          rw [mul_neg, ih, neg_mul_eq_neg_mul]
        · intro y1 y2 ih1 ih2
          rw [mul_add, add_mul, ih1, ih2]
      · intro s ih
        rw [neg_mul, ih, neg_mul_eq_mul_neg]
      · intro x1 x2 ih1 ih2
        rw [add_mul, mul_add, ih1, ih2] }
Похожие утверждения