Theorem: Ex113.mul_def (AlgebraI/Groups.lean)

State before:
a b : { z // ‖z‖ = 1 }
⊢ ‖↑a * ↑b‖ = 1
Tactic:
rw [norm_mul, a.prop, b.prop, one_mul]
State after:
no goals