Why are these not definitionally equal?

Stream: general

[Aaron Anderson]

This project is sorry-free except for one theorem at the end of archive/100-theorems-list/83_friendship/char_poly.lean:https://github.com/leanprover-community/mathlib/compare/freek_83_friendship_theorem

[Aaron Anderson]

The sorries in that theorem seem like they should be solvable by refl, but there's some subtle difference in the definitions.

[Aaron Anderson]

Can anybody help figure out how to make lean realize these things are trivially equal, or even better, avoid using transitivity to begin with?

[Scott Morrison]

By removing the classical, I managed to prove one of the remaining sorries with refl.

[Scott Morrison]

The other one I popped out into a lemma immediately above. It looks completely doable, but when I try to rewrite by matrix.map_sub (which is missing, so I added) something goes wrong...

[Scott Morrison]

Even using convert with matrix.map_sub times out, so there is still something definitionally sick hiding in these terms! :-)

[Jalex Stark]

oof

[Jalex Stark]

hmm I'm not sure how to show that (X • 1)^p = X^p • 1 (I'm working on writing this as a sorry)

[Jalex Stark]

I got it with this, which I wasn't able to find in the library

import data.polynomial

universes u v

variables {R : Type v} {A : Type u} [semiring A] [comm_semiring R] [algebra R A]

lemma algebra.smul_pow (a : A) (r : R) (k : ℕ) : (r • a)^k = r^k • a^k :=
begin
  induction k with d hd, simp,
  rw [pow_succ, hd], rw algebra.smul_mul_assoc, simp, rw smul_smul, ring,
end

[Johan Commelin]

Clearly, we need a smul_one simp-lemma

[Jalex Stark]

i have these but i'm not sure how they generalize

import linear_algebra.matrix

open finset matrix
noncomputable theory

universes v
variables (R : Type v)

@[simp]
lemma nat.smul_one [semiring R] (d : ℕ) : d • (1 : R) = (d : R) :=
begin
  induction d with k hk, { simp },
  rw nat.succ_eq_add_one, push_cast,
  rw ← hk, simp [add_smul],
end

@[simp]
lemma int.smul_one  [ring R] (d : ℤ) : d • (1 : R) = (d : R) :=
by apply gsmul_one

[Jalex Stark]

I think something like mat_poly_equiv_coeff_apply can do a chunk of the work here

[Jalex Stark]

yeah, we have to check an equality in matrix n n (polynomial (zmod p)), and it would be "just a computation" if we were thinking of it as matrix n n (zmod p) \otimes polynomial (zmod p)

[Jalex Stark]

so I guess i should go study scott's proof of cayley hamilton more closely

[Johan Commelin]

@Jalex Stark Hmmm, are you sure that it makes a substantial difference? If p is arbitrary, than it's not like you can ask Lean to do the computation for you.

[Jalex Stark]

Sorry, I don't mean that the proof will be dec_trivial, but rather it'll be rwwith several forms of bilinearity of the tensor product

[Jalex Stark]

we sorted this out! one of the several issues was that typeclass inference could not find the appropriate char_p instance, hence #3535