pith. machine review for the scientific record. sign in
def definition def or abbrev

strictModularRealization

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  31def strictModularRealization (n : ℕ) [Fact (1 < n)] : StrictLogicRealization where
  32  Carrier := ZMod n

proof body

Definition body.

  33  Cost := Nat
  34  zeroCost := inferInstance
  35  compare := zmodCost
  36  compose := fun a b => a + b
  37  one := 0
  38  generator := 1
  39  identity_law := zmodCost_self
  40  non_contradiction_law := zmodCost_symm
  41  excluded_middle_law := True
  42  composition_law := True
  43  invariance_law := True
  44  nontrivial_law := by
  45    have hne : (1 : ZMod n) ≠ 0 := by
  46      intro h
  47      have hval := congrArg ZMod.val h
  48      rw [ZMod.val_one n, ZMod.val_zero] at hval
  49      norm_num at hval
  50    simp [zmodCost, hne]
  51

used by (1)

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

depends on (14)

Lean names referenced from this declaration's body.