feat(data/polynomial/coeff): add char_zero instance on polynomials (#…

…13075)

Besides adding the instance, I also added a warning on the difference between `char_zero R` and `char_p R 0` for general semirings.

An example showing the difference is in #13080.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F)

src/algebra/char_p/basic.lean

@@ -18,7 +18,15 @@ universes u v
 
 variables (R : Type u)
 
-/-- The generator of the kernel of the unique homomorphism ℕ → R for a semiring R -/
+/-- The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.
+
+*Warning*: for a semiring `R`, `char_p R 0` and `char_zero R` need not coincide.
+* `char_p R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`;
+* `char_zero R` requires an injection `ℕ ↪ R`.
+
+For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
+`char_zero {0, 1}` does not hold and yet `char_p {0, 1} 0` does.
+ -/
 class char_p [add_monoid R] [has_one R] (p : ℕ) : Prop :=
 (cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)
 

src/algebra/char_zero.lean

@@ -34,7 +34,15 @@ from the natural numbers into it is injective.
 -/
 
 /-- Typeclass for monoids with characteristic zero.
-  (This is usually stated on fields but it makes sense for any additive monoid with 1.) -/
+  (This is usually stated on fields but it makes sense for any additive monoid with 1.)
+
+*Warning*: for a semiring `R`, `char_zero R` and `char_p R 0` need not coincide.
+* `char_zero R` requires an injection `ℕ ↪ R`;
+* `char_p R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
+
+For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
+`char_zero {0, 1}` does not hold and yet `char_p {0, 1} 0` does.
+ -/
 class char_zero (R : Type*) [add_monoid R] [has_one R] : Prop :=
 (cast_injective : function.injective (coe : ℕ → R))
 

src/data/polynomial/coeff.lean

@@ -285,4 +285,7 @@ end
 
 end cast
 
+instance [char_zero R] : char_zero R[X] :=
+{ cast_injective := λ x y, nat_cast_inj.mp }
+
 end polynomial