Theorems · Definition · number theory

AddChar.PrimitiveAddChar.recOn

{R : Type u} →
  [inst : CommRing R] →
    {R' : Type v} →
      [inst_1 : Field R'] →
        {motive : AddChar.PrimitiveAddChar R R' → Sort u_1} →
          (t : AddChar.PrimitiveAddChar R R') →
            ((n : ℕ+) →
                (char : AddChar R (CyclotomicField (↑n) R')) →
                  (prim : char.IsPrimitive) → motive { n := n, char := char, prim := prim }) →
              motive t

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingField