theorem proved term proof

`zero_mem_Radical`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  37@[simp] theorem zero_mem_Radical {n : ℕ} (α : Vec n) :
  38    (fun _ => 0 : Vec n) ∈ Radical α := by

Term-mode proof.

  39  unfold Radical dot
  40  simp
  41

Lean names referenced from this declaration's body.