Proof that x \ne 0 \implies Complex.normSq \ne 0

Stream: Is there code for X?

[Arien Malec]

Getting back into Lean & Mathlib by working through the latest ed of Axler's Linear Algebra. We are first asked to prove that complex numbers follow the expected laws, which I first did by defining de novo MyComplex but I then wanted to show this in terms of the Mathlib definition of Complex. Almost everything is given except for the existence of an additive inverse, which is trivial, and the existence of a multiplicative inverse, which is less trivial, it seems.

I got theorem exists_mul_inv: ∀x : ℂ , x≠ 0 → ∃y, x * y = 1 down to

x: ℂ
h: x ≠ 0
⊢ Complex.normSq x ≠ 0

This is obviously doable to prove from the definition, but I wondered if the complex norm is otherwise proven to follow the usual laws, so that I could show this for normSq?

[Timo Carlin-Burns]

Is this what you're looking for?

import Mathlib.Data.Complex.Basic

example (x: ℂ) (h: x ≠ 0) : Complex.normSq x ≠ 0 := by
  simp [h]
  -- `simp` uses the fact that `Complex.normSq` is defined as a `MonoidWithZeroHom`

#check Complex.normSq -- ℂ →*₀ ℝ

example (x : ℂ) : Complex.normSq x = 0 ↔ x = 0 := map_eq_zero Complex.normSq

[Arien Malec]

Ahhhh. Yes, perfect.