coeff_add

Stream: new members

[Leo Mayer]

How does one do this?

import tactic
import data.polynomial.basic

open polynomial

example (R : Type) [comm_ring R] (f g : polynomial R) (n : ℕ) :
  (f + g).coeff n = (f.coeff n) + (g.coeff n) := sorry

[Riccardo Brasca]

does library_search work? It is surely already in the library.

[Leo Mayer]

That's what I thought, but its not working for me

[Riccardo Brasca]

docs#polynomial.coeff_add

[Alex J. Best]

simp also solves this and simp? tells you the name of the lemma too.

[Leo Mayer]

Thanks! Why would library_search not be able to find that?

[Alex J. Best]

I think it's just especially slow when trying to prove equalities. It just finished for me after a while and did find it indeed.