Theorems · Definition · number theory
AddChar.PrimitiveAddChar.char
{R : Type u} →
[inst : CommRing R] →
{R' : Type v} →
[inst_1 : Field R'] → (self : AddChar.PrimitiveAddChar R R') → AddChar R (CyclotomicField (↑self.n) R')The second projection from PrimitiveAddChar, giving the character.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Fieldstatement and proof · cited by 7,404
- AddCharstatement · cited by 286
- PNat.valstatement · cited by 226
- CyclotomicFieldstatement · cited by 14
- AddChar.PrimitiveAddCharstatement and proof · cited by 7
- AddChar.PrimitiveAddChar.nstatement · cited by 5
Cited by6
Results whose statement or proof uses this declaration.
- AddChar.PrimitiveAddChar.primstatement · cited by 4
- AddChar.FiniteField.primitiveCharproof · cited by 3
- AddChar.FiniteField.primitiveChar_to_Complexproof · cited by 1
- FiniteField.two_pow_cardproof · cited by 1
- Char.card_pow_cardproof · cited by 1
- jacobiSum_mul_jacobiSum_invproof · cited by 0