Theorems · Theorem · number theory

AddChar.PrimitiveAddChar.mk.injEq

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

0 results in Mathlib

Foundations

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

Assumes

CommRingField