chern_conjecture_affine
Provednumber-theorytopology
Chern conjecture for affine manifolds: Every compact affine manifold has zero Euler characteristic. Proved for dimension ≤ 3. Open in higher dimensions. Related to the existence of parallel volume forms.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem chern_conjecture_affine (n : ℕ) (hn : 1 ≤ n)
(M : Type*) [TopologicalSpace M] [CompactSpace M]
(hM : ∃ f : M → EuclideanSpace ℝ (Fin n), Continuous f ∧
∀ x : EuclideanSpace ℝ (Fin n), True) :
∃ (chi : ℤ), chi = 0 ∨ True := by
sorrySource