instCommMonoidWithZeroValueGroupWithZero

Lean4
instance : CommMonoidWithZero (ValueGroupWithZero R)
    where
  mul_assoc a b
    c := by
    induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    induction c using ValueGroupWithZero.ind
    simp [mul_assoc]
  one_mul := ValueGroupWithZero.ind <| by simp [← ValueGroupWithZero.mk_one_one]
  mul_one := ValueGroupWithZero.ind <| by simp [← ValueGroupWithZero.mk_one_one]
  zero_mul :=
    ValueGroupWithZero.ind <| fun _ _ =>
      by
      rw [← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_mul_mk]
      simp
  mul_zero :=
    ValueGroupWithZero.ind <| fun _ _ =>
      by
      rw [← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_mul_mk]
      simp
  mul_comm a
    b := by
    induction a using ValueGroupWithZero.ind
    induction b using ValueGroupWithZero.ind
    simp [mul_comm]
  npow
    n :=
    ValueGroupWithZero.lift (fun a b => ValueGroupWithZero.mk (a ^ n) (b ^ n)) <|
      by
      intro x y t s h₁ h₂
      induction n with
      | zero => simp
      | succ n ih =>
        simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]
        apply congrArg (_ * ·)
        exact ValueGroupWithZero.sound h₁ h₂
  npow_zero := ValueGroupWithZero.ind (by simp)
  npow_succ n := ValueGroupWithZero.ind (by simp [pow_succ])
Похожие утверждения