∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] (n : ℕ+)
  (char : AddChar R (CyclotomicField (↑n) R')) (prim : char.IsPrimitive) (n_1 : ℕ+)
  (char_1 : AddChar R (CyclotomicField (↑n_1) R')) (prim_1 : char_1.IsPrimitive),
  ({ n := n, char := char, prim := prim } = { n := n_1, char := char_1, prim := prim_1 }) = (n = n_1 ∧ char ≍ char_1)