instIsCharPOfIsLeftCancelAddOfCharP

English

Let α be a semiring with additive cancellation, and suppose CharP α n holds. Then α carries the corresponding CharP-n structure in a canonical way.

Русский

Пусть α — полупринод, удовлетворяющий левой отменимости сложения, и пусть выполняется CharP α n. Тогда α естественным образом обладает соответствующей структурой CharP n.

LaTeX

$$$CharP(\alpha, n) \Rightarrow \mathrm{IsCharP}(\alpha, n).$$$

Lean4

instance (α : Type*) [Semiring α] [IsLeftCancelAdd α] (n : ℕ) [CharP α n] : Lean.Grind.IsCharP α n where
  ofNat_ext_iff
    {a b} := by
    rw [Lean.Grind.Semiring.ofNat_eq_natCast, Lean.Grind.Semiring.ofNat_eq_natCast]
    exact CharP.cast_eq_iff_mod_eq α n

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