Documentation Verification Report

QuadraticReciprocity

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_sq_eq_neg_two_iff`, `exists_sq_eq_prime_iff_of_mod_four_eq_one`, `exists_sq_eq_prime_iff_of_mod_four_eq_three`, `exists_sq_eq_two_iff`, `at_neg_two`, `at_two`, `quadratic_reciprocity`, `quadratic_reciprocity'`, `quadratic_reciprocity_one_mod_four`, `quadratic_reciprocity_three_mod_four`	10
Total	10

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sq_eq_neg_two_iff` 📖	mathematical	—	`IsSquare` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `FiniteField.isSquare_neg_two_iff` `card` `Nat.Prime.mod_two_eq_one_iff_ne_two` `Fact.out`
`exists_sq_eq_prime_iff_of_mod_four_eq_one` 📖	mathematical	—	`IsSquare` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`eq_or_ne` `legendreSym.eq_one_iff'` `prime_ne_zero` `legendreSym.quadratic_reciprocity_one_mod_four`
`exists_sq_eq_prime_iff_of_mod_four_eq_three` 📖	mathematical	—	`IsSquare` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`legendreSym.eq_one_iff'` `prime_ne_zero` `legendreSym.eq_neg_one_iff'` `legendreSym.quadratic_reciprocity_three_mod_four`
`exists_sq_eq_two_iff` 📖	mathematical	—	`IsSquare` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `FiniteField.isSquare_two_iff` `card` `Nat.Prime.mod_two_eq_one_iff_ne_two` `Fact.out`

legendreSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`at_neg_two` 📖	mathematical	—	`legendreSym` `DFunLike.coe` `MulChar` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `MulChar.instFunLike` `ZMod.χ₈'` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_1` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `quadraticChar_neg_two` `ZMod.ringChar_zmod_n` `ZMod.card`
`at_two` 📖	mathematical	—	`legendreSym` `DFunLike.coe` `MulChar` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `MulChar.instFunLike` `ZMod.χ₈` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `Int.cast_ofNat` `eq_1` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `quadraticChar_two` `ZMod.ringChar_zmod_n` `ZMod.card`
`quadratic_reciprocity` 📖	mathematical	—	`legendreSym` `Monoid.toNatPow` `Int.instMonoid`	—	`Nat.Prime.eq_two_or_odd` `Fact.out` `ZMod.ringChar_zmod_n` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `quadraticChar_odd_prime` `Int.cast_natCast` `Nat.cast_one` `eq_1` `ZMod.card` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `mul_rotate'` `mul_comm` `pow_two` `quadraticChar_sq_one` `ZMod.prime_ne_zero` `mul_one` `pow_mul` `ZMod.χ₄_eq_neg_one_pow` `map_pow` `quadraticChar_neg_one`
`quadratic_reciprocity'` 📖	mathematical	—	`legendreSym` `Monoid.toNatPow` `Int.instMonoid`	—	`eq_or_ne` `eq_zero_iff` `Nat.cast_zero` `Int.cast_zero` `Int.cast_natCast` `ZMod.natCast_self` `MulZeroClass.mul_zero` `quadratic_reciprocity` `ZMod.prime_ne_zero` `mul_assoc` `sq_one` `mul_one`
`quadratic_reciprocity_one_mod_four` 📖	mathematical	—	`legendreSym`	—	`quadratic_reciprocity'` `Nat.Prime.mod_two_eq_one_iff_ne_two` `Fact.out` `Nat.odd_of_mod_four_eq_one` `pow_mul` `ZMod.neg_one_pow_div_two_of_one_mod_four` `one_pow` `one_mul`
`quadratic_reciprocity_three_mod_four` 📖	mathematical	—	`legendreSym`	—	`ZMod.neg_one_pow_div_two_of_three_mod_four` `quadratic_reciprocity'` `Nat.Prime.mod_two_eq_one_iff_ne_two` `Fact.out` `Nat.odd_of_mod_four_eq_three` `pow_mul` `neg_one_mul`

---

← Back to Index