more duplicate lemmas

Stream: general

[Tian Chen]

I've noticed some duplicates:

• docs#polynomial.zero_le_degree_iff and docs#polynomial.degree_nonneg_iff_ne_zero which is right under it
• docs#linear_map.to_matrix_apply and docs#linear_map.to_matrix_apply' (similarly, docs#linear_map.to_matrix_transpose_apply and docs#linear_map.to_matrix_transpose_apply')

Which of the first 2 should be removed?

[Eric Wieser]

I think #7496 (cc @Anne Baanen) is at fault in the second bullet; the lemmas used to be different, but a refactor made them the same.

[Junyan Xu]

The duplicate degree_nonneg_iff_ne_zero was added in #3193
polynomial.zero_le_degree_iff has been there for 4 years since #514