theorem proved term proof

`modulus_pos`

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

formal statement (Lean)

  34theorem modulus_pos (k : ℕ) : 0 < modulus k := by

Term-mode proof.

  35  unfold modulus
  36  omega
  37

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

cycStep in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
modularInterpret 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.