OnModCases

Mathlib.Tactic.ModCases

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ModCases.NatMod.OnModCases

Lean4

/-- `OnModCases n a lb p` represents a partial proof by cases that
there exists `0 ≤ m < n` such that `a ≡ m (mod n)`.
It asserts that if `∃ m, lb ≤ m < n ∧ a ≡ m (mod n)` holds, then `p`
(where `p` is the current goal).
-/
def OnModCases (n : ℕ) (a : ℕ) (lb : ℕ) (p : Sort _) :=
  ∀ m, lb ≤ m ∧ m < n ∧ a ≡ m [MOD n] → p

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

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

Разделы

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

Аффилиация

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