English
If R and S both have characteristic exponent p, then the product R × S also has characteristic exponent p. In particular, the property is preserved under finite direct products.
Русский
Если у колец R и S характеристика-экспонента p, то у произведения R × S также характеристика-экспонента p. В частности, свойство сохраняется под конечными прямыми произведениями.
LaTeX
$$$\mathrm{ExpChar}(R \times S, p) \quad\text{whenever}\quad \mathrm{ExpChar}(R, p) \land \mathrm{ExpChar}(S, p).$$$
Lean4
instance (S : Type*) [Semiring S] (p) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p :=
by
obtain hp | ⟨hp⟩ := ‹ExpChar R p›
· constructor
obtain _ | _ := ‹ExpChar S p›
· exact (Nat.not_prime_one hp).elim
· have := Prod.charP R S p; exact .prime hp
