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

State before:
a : { z // ‖z‖ = 1 }
⊢ ‖(↑a)⁻¹‖ = 1
Tactic:
rw [norm_inv, a.prop, inv_one]
State after:
no goals