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

modular_arithmetic_invariant

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)

  82noncomputable def modular_arithmetic_invariant (n : ℕ) [Fact (1 < n)]
  83    (R : LogicRealization.{0, 0}) :
  84    (arithmeticOf (modularRealization n)).peano.carrier
  85      ≃ (arithmeticOf R).peano.carrier :=

proof body

Definition body.

  86  ArithmeticOf.equivOfInitial (arithmeticOf (modularRealization n)) (arithmeticOf R)
  87
  88end ModularRealization
  89end UniversalForcing
  90end Foundation
  91end IndisputableMonolith

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.