char_p instance on polynomials

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is the instance below already available? I tried looking for it, but failed, possibly due to lacking imports.

Thanks!

import data.polynomial.basic
import algebra.char_p.basic

open polynomial
open_locale polynomial

instance polynomial.char_p {R : Type*} [semiring R] {p : ℕ} [char_p R p] : char_p R[X] p :=
{ cast_eq_zero_iff := λ x, by rw [← C_eq_nat_cast, ← C_0, C_inj, ← char_p.cast_eq_zero_iff R] }

[Yaël Dillies]

docs#polynomial.char_p ?

[Yaël Dillies]

You're just too good at naming, Damiano :grinning:

[Damiano Testa]

I did not think of looking in ring_theory, given the fact that there is data.polynomial... my bad!

[Notification Bot]

12 messages were moved from this topic to #general > Rearranging files in data/ by Anne Baanen.