`modular_interpret_periodic`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ModularLogicRealization
domain: Foundation
line: 108 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ModularLogicRealization on GitHub at line 108.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 105    (UniversalForcing.arithmeticOf R)
 106
 107/-- The modular interpretation is periodic on the carrier. -/
 108theorem modular_interpret_periodic (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
 109    modularInterpret k
 110        (ArithmeticFromLogic.LogicNat.fromNat
 111          (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
 112      = modularInterpret k n := by
 113  apply Fin.ext
 114  simp [modularInterpret, ArithmeticFromLogic.LogicNat.toNat_fromNat]
 115
 116end ModularLogicRealization
 117end Foundation
 118end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.