lemma proved term proof

`log2_two`

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

formal statement (Lean)

  42lemma log2_two : log2 2 = 1 := Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)

Term-mode proof.

  43
  44/-- log₂(1/2) = -1 -/

Lean names referenced from this declaration's body.