charP — Mathlib

English

The product of rings has characteristic equal to the lcm of the factors’ characteristics (symmetry version).

Русский

Характеристика произведения колец равна НОК характеристик факторов (симметрическая версия).

LaTeX

$$[CharP S q] ⇒ CharP (R × S) (Nat.lcm p q)$$

Lean4

/-- The characteristic of the product of two rings of the same characteristic
  is the same as the characteristic of the rings -/
instance charP [CharP S p] : CharP (R × S) p := by convert Nat.lcm.charP R S p p; simp

Похожие утверждения