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

norm_div_norm_eq_one

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)

 166theorem norm_div_norm_eq_one : ∀ (z : ℂ), z ≠ 0 → ‖z / ‖z‖‖ = 1 := by

proof body

Tactic-mode proof.

 167  intro z hz
 168  rw [norm_div]
 169  have h1 : ‖(‖z‖ : ℂ)‖ = ‖z‖ := by simp [Complex.norm_real]
 170  rw [h1]
 171  exact div_self (norm_ne_zero_iff.mpr hz)
 172
 173/-- Commit a ledger to a specific outcome.
 174    This is the formal model of wavefunction collapse. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.