theorem
proved
term proof
sub_mem_Radical
show as:
view Lean formalization →
formal statement (Lean)
67theorem sub_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
68 (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
69 v - w ∈ Radical α := by
proof body
Term-mode proof.
70 simpa [sub_eq_add_neg] using
71 add_mem_Radical α hv (smul_mem_Radical α (-1) hw)
72
73/-- The Hessian quadratic form vanishes exactly on the radical distribution. -/