def definition def or abbrev

`modularInterpret`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  47def modularInterpret (k : ℕ) (n : ArithmeticFromLogic.LogicNat) : Fin (modulus k) :=

Definition body.

  48  ⟨ArithmeticFromLogic.LogicNat.toNat n % modulus k, Nat.mod_lt _ (modulus_pos k)⟩
  49

From the project-wide theorem graph. These declarations reference this one in their body.

modular_interpret_periodic in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
modularInterpret_step in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
modularInterpret_zero in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
modularRealization in IndisputableMonolith.Foundation.ModularLogicRealization decl_use

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
modulus in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
modulus_pos in IndisputableMonolith.Foundation.ModularLogicRealization decl_use