nat.smul_one_eq_coe

Stream: new members

[Alex Zhang]

When I was dealing with matrices, I found that @[simp] might be a bad tag for

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] (m : ℕ) :
  m • (1 : R) = ↑m :=
by rw [nsmul_eq_mul, mul_one]
@[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] (m : ℤ) :
  m • (1 : R) = ↑m :=
by rw [gsmul_eq_mul, mul_one]

as the simplified result forbids me from using properties of identity matrices and then using the properties of scalar multiplication.
I temporarily failed to extract a true #mwe to illustrate this.
example [decidable_eq I] (n : ℕ) {i j : I} (h : i ≠ j) : (n • (1 : matrix I I ℚ)) = 0 := by {simp,}
After simp, the LHS changes to ↑n : matrix I I \Q, which is not very convenient to tackle.
When I was doing a more complicated example, I was facing

F: Type u_11
_inst_8: fintype F
_inst_9: decidable_eq F
ij: F
h: i ≠ j
⊢ ↑(card F) i j = 0

and was not quite sure how to continue.
I then carefully used simp only to avoid this stage.

[Eric Wieser]

One way to resolve this would be to add a simp lemma to matrices saying that (coe n) = diagonal (coe n)

[Eric Wieser]

And then there are lots of lemmas about diagonals that would apply

[Eric Wieser]

But you are also right in questioning whether those are sensible simp lemmas, it's not obvious whether they are to me.

[Anne Baanen]

In general coe is the preferred way to convert numbers from concrete types like ℕ. (In particular, we also have simp lemmas saying all ring homs from ℕ / ℤ are equal to coe.) So I don't think that these simp lemmas really are the issue, it's more that there are not enough lemmas about the coe into matrices.

[Alex Zhang]

Good suggestions! If there is going to be any relevant change to mathlib, please let me know.

[Alex Zhang]

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] (m : ℕ) :
  m • (1 : R) = ↑m :=
by rw [nsmul_eq_mul, mul_one]

This applies to other semirings like matrices. So with the simp tag, we may need more lemmas like (coe n) = diagonal (coe n) for other semirings.

[Alex Zhang]

As such, personally, I think removing the simp tag there may be more convenient for the users.

[Yakov Pechersky]

Why not write a matrix.coe_apply?

[Yakov Pechersky]

That would be the simp lemma to add.

[Eric Wieser]

Alex Zhang said:

This applies to other semirings like matrices. So with the simp tag, we may need more lemmas like (coe n) = diagonal (coe n) for other semirings.

Not many other semiring have a diagonal ;)

[Eric Wieser]

Yakov Pechersky said:

That would be the simp lemma to add.

That's certainly a good simp lemma to start with and would resolve the case in question, although I suspect it's more useful to unfold it to diagonal first, otherwise you have to copy every simp lemma about diagonal too