charP — Mathlib

English

The characteristic of a product of rings is the least common multiple of the individual characteristics.

Русский

Характеристика произведения колец равна наименьшему общему кратному характеристикам каждого из колец.

LaTeX

$$$ CharP (R \times S) (Nat.lcm p q) $ given $ CharP R p$ and $CharP S q$$$

Lean4

/-- The characteristic of the product of rings is the least common multiple of the
characteristics of the two rings. -/
instance charP [CharP S q] : CharP (R × S) (Nat.lcm p q) where
  cast_eq_zero_iff := by simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]

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