Zulip Chat Archive

Stream: new members

Topic: gsmul_int_int


Scott Morrison (Mar 07 2020 at 04:11):

argh... can anyone help with:

import algebra.group_power

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

Kenny Lau (Mar 07 2020 at 04:33):

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 (Mar 07 2020 at 05:33):

import algebra.group_power

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

Last updated: Dec 20 2023 at 11:08 UTC