JacobiSymbol

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

Statistics

Metric	Count
Definitions «termJ(_|_)»»), qrSign	2
Theorems isSquare_of_jacobiSym_eq_one, nonsquare_iff_jacobiSym_eq_neg_one, nonsquare_of_jacobiSym_eq_neg_one, at_neg_one, at_neg_two, at_two, div_four_left, eq_neg_one_at_prime_divisor_of_eq_neg_one, eq_one_or_neg_one, eq_zero_iff, eq_zero_iff_not_coprime, even_odd, to_jacobiSym, list_prod_left, list_prod_right, mod_left, mod_left', mod_right, mod_right', mul_left, mul_right, mul_right', ne_zero, neg, one_left, one_right, pow_left, pow_right, prime_dvd_of_eq_neg_one, quadratic_reciprocity, quadratic_reciprocity', quadratic_reciprocity_if, quadratic_reciprocity_one_mod_four, quadratic_reciprocity_one_mod_four', quadratic_reciprocity_three_mod_four, sq_one, sq_one', trichotomy, value_at, zero_left, zero_right, eq_iff_eq, mul_left, mul_right, neg_one_pow, sq_eq_one	46
Total	48

NumberTheorySymbols

Definitions

Name	Category	Theorems
«termJ(_|_)» 📖» "API Documentation")	CompOp	—

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSquare_of_jacobiSym_eq_one 📖	mathematical	jacobiSym	IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField	—	nonsquare_iff_jacobiSym_eq_neg_one
nonsquare_iff_jacobiSym_eq_neg_one 📖	mathematical	—	jacobiSym IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField	—	jacobiSym.legendreSym.to_jacobiSym legendreSym.eq_neg_one_iff
nonsquare_of_jacobiSym_eq_neg_one 📖	mathematical	jacobiSym	IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	jacobiSym.mod_left sq intCast_eq_intCast_iff' Int.cast_mul coe_valMinAbs jacobiSym.pow_left sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instAddLeftMono

(root)

Definitions

Name	Category	Theorems
qrSign 📖	CompOp	7 math math: qrSign.neg_one_pow, qrSign.sq_eq_one, qrSign.symm, qrSign.eq_iff_eq, qrSign.mul_left, qrSign.mul_right, jacobiSym.quadratic_reciprocity'

jacobiSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
at_neg_one 📖	mathematical	Odd Nat.instSemiring	jacobiSym DFunLike.coe MulChar ZMod CommRing.toCommMonoid ZMod.commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike ZMod.χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	value_at legendreSym.at_neg_one
at_neg_two 📖	mathematical	Odd Nat.instSemiring	jacobiSym DFunLike.coe MulChar ZMod CommRing.toCommMonoid ZMod.commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike ZMod.χ₈' AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	value_at legendreSym.at_neg_two
at_two 📖	mathematical	Odd Nat.instSemiring	jacobiSym DFunLike.coe MulChar ZMod CommRing.toCommMonoid ZMod.commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike ZMod.χ₈ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	value_at legendreSym.at_two
div_four_left 📖	mathematical	—	jacobiSym	—	mul_left sq_one' one_mul
eq_neg_one_at_prime_divisor_of_eq_neg_one 📖	mathematical	jacobiSym	Nat.Prime	—	one_ne_zero CharZero.eq_neg_self_iff NormMulClass.toNoZeroDivisors Int.instNormMulClass Int.instCharZero zero_right LT.lt.ne Nat.pos_of_mem_primeFactorsList List.neg_one_mem_of_prod_eq_neg_one list_prod_right Nat.prod_primeFactorsList Nat.prime_of_mem_primeFactorsList Nat.dvd_of_mem_primeFactorsList
eq_one_or_neg_one 📖	mathematical	—	jacobiSym	—	trichotomy ne_zero
eq_zero_iff 📖	mathematical	—	jacobiSym	—	eq_or_ne zero_right ne_zero eq_zero_iff_not_coprime
eq_zero_iff_not_coprime 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList List.prod_eq_zero_iff Int.instNontrivial NormMulClass.toNoZeroDivisors Int.instNormMulClass Int.gcd_eq_natAbs Nat.Prime.not_coprime_iff_dvd legendreSym.eq_zero_iff Nat.mem_primeFactorsList
even_odd 📖	mathematical	—	jacobiSym	—	mul_left at_two Nat.odd_iff ZMod.χ₈_nat_eq_if_mod_eight
list_prod_left 📖	mathematical	—	jacobiSym AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	one_left mul_left
list_prod_right 📖	mathematical	—	jacobiSym Nat.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	one_right List.prod_ne_zero Nat.instNontrivial IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing mul_right'
mod_left 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList legendreSym.mod Nat.dvd_of_mem_primeFactorsList
mod_left' 📖	mathematical	—	jacobiSym	—	mod_left
mod_right 📖	mathematical	Odd Nat.instSemiring	jacobiSym	—	mod_right' Odd.mod_even Even.mul_right Distrib.rightDistribClass neg ZMod.χ₄_nat_mod_four dvd_mul_right
mod_right' 📖	mathematical	Odd Nat.instSemiring	jacobiSym	—	eq_or_ne MulZeroClass.mul_zero Odd.mod_even Even.mul_right Distrib.rightDistribClass Nat.exists_eq_pow_mul_and_not_dvd Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Nat.odd_iff Nat.two_dvd_ne_zero Nat.cast_mul mul_left quadratic_reciprocity' Nat.cast_pow pow_left Nat.cast_two at_two pow_zero ZMod.χ₈_nat_mod_eight Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw ZMod.χ₄_nat_mod_four dvd_mul_right mod_left Int.natCast_mod dvd_mul_left
mul_left 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList legendreSym.mul List.prod_map_mul
mul_right 📖	mathematical	—	jacobiSym	—	mul_right'
mul_right' 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList eq_1 List.Perm.prod_eq Nat.perm_primeFactorsList_mul
ne_zero 📖	—	—	—	—	eq_zero_or_neZero zero_right one_ne_zero Mathlib.Tactic.Contrapose.contrapose₃ eq_zero_iff_not_coprime
neg 📖	mathematical	Odd Nat.instSemiring	jacobiSym DFunLike.coe MulChar ZMod CommRing.toCommMonoid ZMod.commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike ZMod.χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	neg_eq_neg_one_mul mul_left at_neg_one
one_left 📖	mathematical	—	jacobiSym	—	List.prod_eq_one Nat.prime_of_mem_primeFactorsList legendreSym.at_one
one_right 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList Nat.primeFactorsList_one
pow_left 📖	mathematical	—	jacobiSym Monoid.toNatPow Int.instMonoid	—	pow_zero one_left pow_succ mul_left
pow_right 📖	mathematical	—	jacobiSym Monoid.toNatPow Nat.instMonoid Int.instMonoid	—	pow_zero one_right eq_zero_or_neZero zero_pow zero_right one_pow pow_succ mul_right
prime_dvd_of_eq_neg_one 📖	—	jacobiSym Monoid.toNatPow Int.instMonoid	—	—	legendreSym.prime_dvd_of_eq_neg_one legendreSym.to_jacobiSym
quadratic_reciprocity 📖	mathematical	Odd Nat.instSemiring	jacobiSym Monoid.toNatPow Int.instMonoid	—	qrSign.neg_one_pow qrSign.symm quadratic_reciprocity'
quadratic_reciprocity' 📖	mathematical	Odd Nat.instSemiring	jacobiSym qrSign	—	one_left mul_one qrSign.mul_left Nat.cast_mul mul_left mul_mul_mul_comm value_at Nat.Prime.eq_two_or_odd' legendreSym.to_jacobiSym Nat.cast_id qrSign.eq_iff_eq qrSign.symm qrSign.neg_one_pow legendreSym.quadratic_reciprocity'
quadratic_reciprocity_if 📖	mathematical	—	jacobiSym	—	Nat.odd_mod_four_iff Nat.instCharZero Nat.instAtLeastTwoHAddOfNat quadratic_reciprocity_one_mod_four' Nat.odd_iff quadratic_reciprocity_one_mod_four quadratic_reciprocity_three_mod_four
quadratic_reciprocity_one_mod_four 📖	mathematical	Odd Nat.instSemiring	jacobiSym	—	quadratic_reciprocity Nat.odd_iff 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_one_mod_four' 📖	mathematical	Odd Nat.instSemiring	jacobiSym	—	quadratic_reciprocity_one_mod_four
quadratic_reciprocity_three_mod_four 📖	mathematical	—	jacobiSym	—	ZMod.neg_one_pow_div_two_of_three_mod_four quadratic_reciprocity Nat.odd_iff Nat.odd_of_mod_four_eq_three pow_mul neg_one_mul
sq_one 📖	mathematical	—	Monoid.toNatPow Int.instMonoid jacobiSym	—	eq_one_or_neg_one
sq_one' 📖	mathematical	—	jacobiSym Monoid.toNatPow Int.instMonoid	—	pow_left sq_one
trichotomy 📖	mathematical	—	jacobiSym	—	Submonoid.list_prod_mem MonoidHom.instMonoidHomClass Set.pair_comm SignType.range_eq Nat.prime_of_mem_primeFactorsList quadraticChar_isQuadratic NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt'
value_at 📖	mathematical	legendreSym Nat.Prime DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Int.instSemiring MonoidHom.instFunLike AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Odd Nat.instSemiring	jacobiSym	—	Nat.prod_primeFactorsList LT.lt.ne' Odd.pos Nat.instCanonicallyOrderedAdd Nat.instNontrivial Nat.cast_list_prod map_list_prod MonoidHom.instMonoidHomClass Nat.prime_of_mem_primeFactorsList eq_1 Odd.ne_two_of_dvd_nat Nat.dvd_of_mem_primeFactorsList
zero_left 📖	mathematical	—	jacobiSym	—	eq_zero_iff_not_coprime ne_zero_of_lt LT.lt.ne'
zero_right 📖	mathematical	—	jacobiSym	—	Nat.prime_of_mem_primeFactorsList Nat.primeFactorsList_zero

jacobiSym.legendreSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_jacobiSym 📖	mathematical	—	legendreSym jacobiSym	—	Nat.prime_of_mem_primeFactorsList Nat.primeFactorsList_prime Fact.out mul_one

qrSign

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iff_eq 📖	mathematical	Odd Nat.instSemiring	qrSign	—	mul_assoc pow_two sq_eq_one one_mul
mul_left 📖	mathematical	—	qrSign	—	Nat.cast_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass jacobiSym.mul_left
mul_right 📖	mathematical	—	qrSign	—	jacobiSym.mul_right
neg_one_pow 📖	mathematical	Odd Nat.instSemiring	qrSign Monoid.toNatPow Int.instMonoid	—	eq_1 pow_mul ZMod.χ₄_eq_neg_one_pow Nat.odd_iff Nat.odd_mod_four_iff ZMod.χ₄_nat_one_mod_four jacobiSym.one_left one_pow ZMod.χ₄_nat_three_mod_four jacobiSym.at_neg_one
sq_eq_one 📖	mathematical	Odd Nat.instSemiring	Monoid.toNatPow Int.instMonoid qrSign	—	neg_one_pow pow_mul mul_comm neg_one_sq one_pow

---

← Back to Index