GaussSum

📁 Source: Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean

Statistics

Metric	Count
Definitions	0
Theorems isSquare_neg_two_iff, isSquare_odd_prime_iff, isSquare_two_iff, quadraticChar_card_card, quadraticChar_neg_two, quadraticChar_odd_prime, quadraticChar_two	7
Total	7

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSquare_neg_two_iff 📖	mathematical	—	IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat even_card_of_char_two isSquare_of_char_two Finite.of_fintype odd_card_of_char_ne_two quadraticChar_one_iff_isSquare neg_ne_zero Ring.two_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing quadraticChar_neg_two ZMod.χ₈'_nat_eq_if_mod_eight
isSquare_odd_prime_iff 📖	mathematical	—	IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' eq_or_ne card ringChar.charP CharP.cast_eq_zero Nat.cast_pow ZMod.charP zero_pow MulZeroClass.mul_zero MulCharClass.map_nonunit MulChar.instMulCharClass Iff.not_left quadraticChar_neg_one_iff_not_isSquare quadraticChar_odd_prime
isSquare_two_iff 📖	mathematical	—	IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat even_card_of_char_two isSquare_of_char_two Finite.of_fintype odd_card_of_char_ne_two quadraticChar_one_iff_isSquare Ring.two_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing quadraticChar_two ZMod.χ₈_nat_eq_if_mod_eight

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quadraticChar_card_card 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Fintype.card Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddGroupWithOne.toIntCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	—	quadraticChar_exists_neg_one' MulChar.ne_one_iff eq_intCast RingHom.instRingHomClass Int.cast_neg Int.cast_one Ring.neg_one_ne_one_of_char_ne_two IsLocalRing.toNontrivial Field.instIsLocalRing Char.card_pow_card MulChar.IsQuadratic.comp quadraticChar_isQuadratic MulChar.IsQuadratic.eq_of_eq_coe quadraticChar_eq_pow_of_char_ne_two'
quadraticChar_neg_two 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat ZMod ZMod.commRing ZMod.χ₈' CommRing.toRing Fintype.card	—	Nat.instAtLeastTwoHAddOfNat neg_mul one_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass ZMod.χ₈'_eq_χ₄_mul_χ₈ quadraticChar_neg_one quadraticChar_two ZMod.cast_natCast ZMod.charP
quadraticChar_odd_prime 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod ZMod.instField ZMod.fintype NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' ZMod.decidableEq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast ZMod.χ₄ CommRing.toRing Fintype.card	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' quadraticChar_neg_one quadraticChar_card_card ne_of_eq_of_ne ZMod.ringChar_zmod_n ZMod.card
quadraticChar_two 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat ZMod ZMod.commRing ZMod.χ₈ CommRing.toRing Fintype.card	—	MulChar.IsQuadratic.eq_of_eq_coe quadraticChar_isQuadratic ZMod.isQuadratic_χ₈ IsLocalRing.toNontrivial Field.instIsLocalRing Nat.instAtLeastTwoHAddOfNat quadraticChar_eq_pow_of_char_ne_two' FiniteField.two_pow_card

---

← Back to Index