intCast_eq_mod

Mathlib.Tactic.ReduceModChar

URI: https://scilib.ai/kg/mathlib#Tactic.ReduceModChar.CharP.intCast_eq_mod

Lean4

theorem intCast_eq_mod (R : Type _) [Ring R] (p : ℕ) [CharP R p] (k : ℤ) : (k : R) = (k % p : ℤ) :=
  CharP.intCast_eq_intCast_mod R p

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

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

Разделы

Аффилиация

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