pith. machine review for the scientific record. sign in
theorem proved term proof

chern_number_integer_from_8tick

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)

  51theorem chern_number_integer_from_8tick :
  52    -- The 8-tick phase ω^8 = 1 forces integer winding numbers
  53    ∀ k : Fin 8, ∃ n : ℤ, (phaseExp k)^8 = 1 := by

proof body

Term-mode proof.

  54  intro k
  55  exact ⟨1, phase_eighth_power_is_one k⟩
  56
  57/-! ## IQHE - Integer Quantum Hall Effect -/
  58
  59/-- **IQHE FILLING FACTOR**: ν = n (integer) when n Landau levels are filled. -/

depends on (8)

Lean names referenced from this declaration's body.