natCast_eq_natCast_mod

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#CharP.natCast_eq_natCast_mod

English

In a ring with CharP R p, the natural number a casts to R as a mod p residue: (a : R) = a mod p.

Русский

В кольце с CharP R p для натурального числа a изображение a в R равно остатку a по модулю p: (a : R) = a mod p.

LaTeX

$$$ (a : R) = a \bmod p $$$

Lean4

theorem natCast_eq_natCast_mod (a : ℕ) : (a : R) = a % p :=
  natCast_eq_natCast' R p (Nat.mod_modEq a p).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru