intCast_eq_intCast_mod

Mathlib.Algebra.CharP.Basic

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

English

For any integer a, (a : R) equals a mod p, i.e. (a : R) = a mod p.

Русский

Для любого целого a получается (a : R) = a mod p.

LaTeX

$$$ (a : R) = a \;\%\ (p : \mathbb{Z}) $$$

Lean4

theorem intCast_eq_intCast_mod : (a : R) = a % (p : ℤ) :=
  (CharP.intCast_eq_intCast R p).mpr (Int.mod_modEq a p).symm

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

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

Разделы

Аффилиация

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