Theorem: GaussInt.norm_conj (MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
x : GaussInt
⊢ x.conj.norm = x.norm
Tactic:
simp [norm]
State after:
no goals