gsmul API

Stream: Is there code for X?

[Kevin Buzzard]

Sorry I am so rubbish. I need things like

import tactic

universe uA

lemma gsmul_univ_apply₂ {A : Type uA} [add_group A] (F : ℤ → A → A) (F_zero : ∀ a, F 0 a = 0)
  (F_succ : ∀ (n : ℕ) (a : A), F (n.succ : ℕ) a = a + F n a)
  (F_neg : ∀ (n : ℕ) (a : A), F -[1+ n] a = -F (n.succ : ℕ) a) (z : ℤ) (a : A) :
  F z a = gsmul z a := sorry

lemma gsmul_univ {A : Type uA} [add_group A] (F : ℤ → A → A) (F_zero : ∀ a, F 0 a = 0)
  (F_succ : ∀ (n : ℕ) (a : A), F (n.succ : ℕ) a = a + F n a)
  (F_neg : ∀ (n : ℕ) (a : A), F -[1+ n] a = -F (n.succ : ℕ) a) : F = gsmul :=
sorry

lemma pred_smul (n : ℤ) (A : Type) [add_group A] (a : A) :
  (n - 1) • a = n • a - a := sorry

I am faced with goals such as

@[simp] lemma int_smul_apply (c : some_bundled_function X -> M) (z : ℤ) (g : X) :
  (z • c) g = z • (c g) :=sorry

and the proof is "there is only wont int action on anything but my simps aren't getting me anywhere; I need to know some tricks I think.

[Kevin Buzzard]

lemma smul_gsmul (G M : Type) [group G] [add_comm_group M] [distrib_mul_action G M]
  (g : G) (n : ℤ) (m : M) : g • n • m = n • g • m := sorry

[Kevin Buzzard]

lemma smul_gsmul (G M : Type) [group G] [add_comm_group M] [distrib_mul_action G M]
  (g : G) (n : ℤ) (m : M) : g • n • m = n • g • m :=
int.induction_on n
  ( by simp)
  ( λ i h, by { simp only [add_smul, smul_add, add_left_inj, one_gsmul, h] })
  ( λ i h, by { simp only [pred_smul, smul_sub, smul_neg, neg_inj, sub_left_inj, h] } )

Is this what I'm supposed to be doing?

[Scott Morrison]

Do the nsmul versions exist? Perhaps it's possible to avoid an induction and just do a case split then rely on the nsmul versions.

[Eric Wieser]

int_smul_apply is usually true by rfl

[Eric Wieser]

smul_gsmul is just a special case of smul_comm, suggesting you should really be providing an smul_comm_class instance

[Eric Wieser]

But I think we already have docs#add_comm_group.int_smul_comm_class.