normIntNumeral

Mathlib.Tactic.ReduceModChar

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

Lean4

/-- Given an integral expression `e : t` such that `t` is a ring of characteristic `n`,
reduce `e` modulo `n`. -/
partial def normIntNumeral {α : Q(Type u)} (n : Q(ℕ)) (e : Q($α)) (_ : Q(Ring $α)) (instCharP : Q(CharP $α $n)) :
    MetaM (Result e) := do
  let ⟨n', pn⟩ ← deriveNat n q(instAddMonoidWithOneNat)
  normIntNumeral' n n' pn e _ instCharP

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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