Theorems · Theorem · number theory

AddChar.PrimitiveAddChar.mk.sizeOf_spec

∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] [inst_2 : SizeOf R] [inst_3 : SizeOf R'] (n : ℕ+)
  (char : AddChar R (CyclotomicField (↑n) R')) (prim : char.IsPrimitive),
  sizeOf { n := n, char := char, prim := prim } = 1 + sizeOf n + sizeOf char

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFieldSizeOfSizeOf