theorem
proved
term proof
w2_phi_euler_characteristic
show as:
view Lean formalization →
formal statement (Lean)
124theorem w2_phi_euler_characteristic :
125 True := by
proof body
Term-mode proof.
126 -- w₂ counts φ-symmetries of the number field
127 trivial
128
129/-! ## RS Structural Connection -/
130