Theorems · Theorem · number theory

AddChar.PrimitiveAddChar.mk.inj

∀ {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

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

1 results in Mathlib

Foundations

Depth 216 from the axioms · uses propext, Classical.choice, Quot.sound