gsmul_int_int

Stream: new members

[Scott Morrison]

argh... can anyone help with:

import algebra.group_power

lemma gsmul_int_int (a b : ℤ) : gsmul a b = a * b := sorry

[Kenny Lau]

import algebra.group_power

lemma gsmul_int_int (a b : ℤ) : gsmul a b = a * b :=
int.induction_on a
  (by rw [zero_gsmul, zero_mul])
  (λ i ih, by rw [add_one_gsmul, ih, add_mul, one_mul])
  (λ i ih, by rw [sub_eq_add_neg, add_gsmul, ih, neg_one_gsmul, add_mul, neg_one_mul])

[Mario Carneiro]

import algebra.group_power

lemma gsmul_int_int (a b : ℤ) : gsmul a b = a * b := by simp [gsmul_eq_mul]