Non_Zero_Elements_of_Division_Ring_form_Group
Proveddivision-ringsgroupsproofwiki
Let R be a division ring. Then (R*, *) is a group.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Non_Zero_Elements_of_Division_Ring_form_Group {R : Type _} [DivisionRing R] (a b : R) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by sorrySource