zsmul lemmas

Stream: new members

[Yakov Pechersky]

Do we really not have these?

import algebra.group_power.order
import algebra.smul_with_zero

variables {R : Type*}

lemma succ_zsmul [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = x + n • x := sorry

lemma succ_zsmul' [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = n • x + x := sorry

[Yakov Pechersky]

I only proved them after importing data.int.basic:

import algebra.group_power.order
import algebra.smul_with_zero
import data.int.basic

@[simp] lemma int.neg_succ_zero : -[1+ 0] = -1 := rfl
@[simp] lemma int.neg_succ_succ_succ (n : ℕ) : -[1+ n.succ] + 1 = -[1+ n] := rfl

variables {R : Type*}

lemma succ_zsmul [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = x + n • x :=
begin
  cases n,
  { rw [←int.of_nat_succ, of_nat_zsmul, of_nat_zsmul, succ_nsmul] },
  { cases n;
    simp [succ_nsmul'] }
end

lemma succ_zsmul' [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = n • x + x :=
begin
  cases n,
  { rw [←int.of_nat_succ, of_nat_zsmul, of_nat_zsmul, succ_nsmul'] },
  { cases n;
    simp [succ_nsmul] }
end

[Adam Topaz]

Do you want your add_group to be an add_comm_group?

[Yakov Pechersky]

Nope, these should be true even for noncomm add_group.

[Adam Topaz]

import algebra.group_power.order
import algebra.smul_with_zero
import algebra

variables {R : Type*}

lemma succ_zsmul [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = x + n • x := by { rw add_comm n, exact one_add_zsmul x n }

lemma succ_zsmul' [add_group R] (n : ℤ) (x : R) :
  (n + 1) • x = n • x + x := add_one_zsmul x n

[Adam Topaz]

You can probably minimize the algebra import.

[Yakov Pechersky]

Thanks!