structure definition def or abbrev

`K2RingOfIntegers`

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

formal statement (Lean)

  45structure K2RingOfIntegers where
  46  field : Type
  47  order : ℕ  -- |K₂(O_F)|
  48
  49/-- Dedekind zeta function value at -1 -/

Lean names referenced from this declaration's body.

zeta in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use