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

positive_eigenvalue_count

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)

 153theorem positive_eigenvalue_count :
 154    (Finset.univ.filter (fun i : Fin 4 => 0 < η i i)).card = 3 := by

proof body

Term-mode proof.

 155  suffices h : Finset.univ.filter (fun i : Fin 4 => 0 < η i i) =
 156    {(1 : Fin 4), (2 : Fin 4), (3 : Fin 4)} by
 157    rw [h]; decide
 158  ext i; fin_cases i <;>
 159    simp [Finset.mem_filter, η_00, η_11, η_22, η_33, Fin.ext_iff]
 160
 161/-- **SE-004: The metric signature is (1, 3) — Lorentzian.** -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.