theorem rokhlin_signature {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [_hsc : IsCompactSimplyConnected4Manifold M] [htop : Has4ManifoldTopology M] (heven : (Has4ManifoldTopology.Q M).isEven = true) : 16 ∣ (Has4ManifoldTopology.Q M).signature

Rokhlin's theorem: the signature $\sigma(M)$ of a closed simply connected smooth $4$-manifold with even intersection form is divisible by $16$.

theorem donaldson_definite_diagonalizable {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [_hsc : IsCompactSimplyConnected4Manifold M] [htop : Has4ManifoldTopology M] (hdef : (Has4ManifoldTopology.Q M).IsPositiveDefinite) : (Has4ManifoldTopology.Q M).IsDiagonal

Donaldson's diagonalizability theorem (positive definite case): if the intersection form $Q$ of a closed simply connected smooth $4$-manifold is positive definite, then $Q$ is diagonalizable over $\mathbb{Z}$ (i.e. equivalent to the standard form $\mathrm{diag}(1,\ldots,1)$).

theorem donaldson_negdef_diagonalizable {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [_hsc : IsCompactSimplyConnected4Manifold M] [htop : Has4ManifoldTopology M] (hdef : (Has4ManifoldTopology.Q M).IsNegativeDefinite) : (Has4ManifoldTopology.Q M).IsDiagonal

Donaldson's diagonalizability theorem (negative definite case): a negative definite intersection form on a closed simply connected smooth $4$-manifold is diagonalizable over $\mathbb{Z}$ (equivalent to $\mathrm{diag}(-1,\ldots,-1)$).

theorem freedman_homeomorphic_of_same_invariants {M₁ : Type u_1} {M₂ : Type u_2} [TopologicalSpace M₁] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M₁] [TopologicalSpace M₂] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M₂] [_hsc₁ : IsCompactSimplyConnected4Manifold M₁] [_hsc₂ : IsCompactSimplyConnected4Manifold M₂] [htop₁ : Has4ManifoldTopology M₁] [htop₂ : Has4ManifoldTopology M₂] (hb₂ : (Has4ManifoldTopology.Q M₁).b₂ = (Has4ManifoldTopology.Q M₂).b₂) (hσ : (Has4ManifoldTopology.Q M₁).signature = (Has4ManifoldTopology.Q M₂).signature) (hparity : (Has4ManifoldTopology.Q M₁).isEven = (Has4ManifoldTopology.Q M₂).isEven) : AreHomeomorphic4Manifolds M₁ M₂

Freedman's classification: two closed simply connected topological $4$-manifolds with the same $b_2$, signature $\sigma$, and parity of the intersection form are homeomorphic.