Documentation Verification Report

AddCharacter

📁 Source: Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

Statistics

Metric	Count
Definitions `primitiveChar`, `primitiveChar_to_Complex`, `IsPrimitive`, `PrimitiveAddChar`, `char`, `n`, `primitiveZModChar`, `zmodChar`	8
Theorems `primitiveChar_to_Complex_isPrimitive`, `compMulHom_of_isPrimitive`, `of_ne_one`, `zmod_char_eq_one_iff`, `prim`, `exists_divisor_of_not_isPrimitive`, `not_isPrimitive_mulShift`, `starComp_apply`, `starComp_eq_inv`, `sum_eq_card_of_eq_one`, `sum_eq_zero_of_ne_one`, `sum_mulShift`, `to_mulShift_inj_of_isPrimitive`, `val_mem_rootsOfUnity`, `zmodChar_apply`, `zmodChar_apply'`, `zmodChar_primitive_of_primitive_root`, `zmod_char_ne_one_iff`, `zmod_char_primitive_of_eq_one_only_at_zero`	19
Total	27

AddChar

Definitions

Name	Category	Theorems
`IsPrimitive` 📖	MathDef	8 math math: `zmod_char_primitive_of_eq_one_only_at_zero`, `ZMod.isPrimitive_stdAddChar`, `PrimitiveAddChar.prim`, `IsPrimitive.of_ne_one`, `IsPrimitive.compMulHom_of_isPrimitive`, `FiniteField.primitiveChar_to_Complex_isPrimitive`, `zmodChar_primitive_of_primitive_root`, `not_isPrimitive_mulShift`
`PrimitiveAddChar` 📖	CompData	—
`primitiveZModChar` 📖	CompOp	—
`zmodChar` 📖	CompOp	3 math math: `zmodChar_apply'`, `zmodChar_apply`, `zmodChar_primitive_of_primitive_root`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_divisor_of_not_isPrimitive` 📖	mathematical	`IsPrimitive` `ZMod` `ZMod.commRing` `CommRing.toCommMonoid`	`mulShift` `ZMod` `CommRing.toRing` `ZMod.commRing` `CommRing.toCommMonoid` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddChar` `AddMonoidWithOne.toAddMonoid` `CommMonoid.toMonoid` `instOne`	—	`ZMod.eq_unit_mul_divisor` `lt_of_le_of_ne` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `ZMod.natCast_self` `MulZeroClass.mul_zero` `mulShift_unit_eq_one_iff` `mul_comm` `ext` `mulShift_apply` `mul_assoc`
`not_isPrimitive_mulShift` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsPrimitive` `mulShift` `CommRing.toRing`	—	`mulShift_mulShift` `mul_comm` `mulShift_zero`
`starComp_apply` 📖	mathematical	`ringChar` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `instFunLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `Ring.toAddCommGroup` `CommRing.toCommMonoid` `Complex.commRing`	—	`starComp_eq_inv`
`starComp_eq_inv` 📖	mathematical	`ringChar` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`MonoidHom.compAddChar` `Complex` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `RingHom.toMonoidHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `starRingEnd` `Complex.instStarRing` `AddChar` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `Ring.toAddCommGroup` `CommRing.toCommMonoid` `Complex.commRing`	—	`ext` `inv_apply'` `val_isUnit` `Complex.norm_eq_one_of_mem_rootsOfUnity` `NeZero.pnat` `val_mem_rootsOfUnity` `Complex.inv_eq_conj`
`sum_eq_card_of_eq_one` 📖	mathematical	`AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOne`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Fintype.card`	—	`Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul` `mul_one`
`sum_eq_zero_of_ne_one` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`ne_one_iff` `Fintype.sum_bijective` `AddGroup.addLeft_bijective` `eq_zero_of_mul_eq_self_left` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Finset.mul_sum` `Finset.sum_congr` `map_add_eq_mul`
`sum_mulShift` 📖	mathematical	`IsPrimitive` `CommRing.toCommMonoid`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Fintype.card`	—	`Finset.sum_congr` `MulZeroClass.mul_zero` `map_zero_eq_one` `Finset.sum_const` `Nat.smul_one_eq_cast` `mul_comm` `Nat.cast_zero` `sum_eq_zero_of_ne_one`
`to_mulShift_inj_of_isPrimitive` 📖	mathematical	`IsPrimitive`	`AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `CommMonoid.toMonoid` `mulShift`	—	`mulShift_mul` `add_neg_cancel` `mulShift_zero`
`val_mem_rootsOfUnity` 📖	mathematical	`ringChar` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Units` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `PNat.val` `Nat.toPNat'` `ringChar` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsUnit.unit` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instFunLike` `val_isUnit`	—	`val_isUnit` `Nat.toPNat'_coe` `nsmul_eq_mul` `CharP.cast_eq_zero` `ringChar.charP` `MulZeroClass.zero_mul` `map_zero_eq_one`
`zmodChar_apply` 📖	mathematical	`Monoid.toPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `CommMonoid.toMonoid` `instFunLike` `zmodChar` `Monoid.toPow` `ZMod.val`	—	—
`zmodChar_apply'` 📖	mathematical	`Monoid.toPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `CommMonoid.toMonoid` `instFunLike` `zmodChar` `AddMonoidWithOne.toNatCast` `Monoid.toPow`	—	`pow_eq_pow_mod` `zmodChar_apply` `ZMod.val_natCast`
`zmodChar_primitive_of_primitive_root` 📖	mathematical	`IsPrimitiveRoot`	`IsPrimitive` `ZMod` `ZMod.commRing` `zmodChar` `Monoid.toPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsPrimitiveRoot` `IsPrimitiveRoot.iff_def`	—	`zmod_char_primitive_of_eq_one_only_at_zero` `IsPrimitiveRoot.iff_def` `ZMod.val_eq_zero` `ZMod.val_lt` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `pow_zero` `zmodChar_apply`
`zmod_char_ne_one_iff` 📖	—	—	—	—	`ne_one_iff` `Mathlib.Tactic.Contrapose.contrapose₃` `nsmul_eq_mul` `mul_one` `ZMod.natCast_zmod_val` `map_nsmul_eq_pow` `one_pow`
`zmod_char_primitive_of_eq_one_only_at_zero` 📖	mathematical	`ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	`IsPrimitive` `ZMod` `ZMod.commRing`	—	`Nat.cast_one` `mul_one` `mulShift_apply`

AddChar.FiniteField

Definitions

Name	Category	Theorems
`primitiveChar` 📖	CompOp	—
`primitiveChar_to_Complex` 📖	CompOp	1 math math: `primitiveChar_to_Complex_isPrimitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primitiveChar_to_Complex_isPrimitive` 📖	mathematical	—	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `primitiveChar_to_Complex`	—	`AddChar.IsPrimitive.compMulHom_of_isPrimitive` `AddChar.PrimitiveAddChar.prim` `AlgEquiv.injective` `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero` `Complex.instCharZero` `IsSepClosedOfCharZero.isCyclotomicExtension` `IsSepClosed.of_isAlgClosed` `Complex.isAlgClosed`

AddChar.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compMulHom_of_isPrimitive` 📖	mathematical	`AddChar.IsPrimitive` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike`	`AddChar.IsPrimitive` `MonoidHom.compAddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `CommMonoid.toMonoid`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `MonoidHom.compAddChar_injective_right`
`of_ne_one` 📖	mathematical	—	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`AddChar.mulShift_mulShift` `mul_inv_cancel₀` `AddChar.mulShift_one`
`zmod_char_eq_one_iff` 📖	mathematical	`AddChar.IsPrimitive` `ZMod` `ZMod.commRing`	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `CommMonoid.toMonoid` `AddChar.instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`not_imp_comm` `AddChar.zmod_char_ne_one_iff` `AddChar.mulShift_apply` `mul_one` `AddChar.map_zero_eq_one`

AddChar.PrimitiveAddChar

Definitions

Name	Category	Theorems
`char` 📖	CompOp	1 math math: `prim`
`n` 📖	CompOp	1 math math: `prim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prim` 📖	mathematical	—	`AddChar.IsPrimitive` `CyclotomicField` `PNat.val` `n` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instFieldCyclotomicField` `char`	—	—

---

← Back to Index