Basic

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

Statistics

Metric	Count
Definitions legendreSym, hom	2
Theorems euler_criterion, euler_criterion_units, exists_sq_eq_neg_one_iff, mod_four_ne_three_of_sq_eq_neg_one, mod_four_ne_three_of_sq_eq_neg_sq, mod_four_ne_three_of_sq_eq_neg_sq', pow_div_two_eq_neg_one_or_one, at_neg_one, at_one, at_zero, card_sqrts, eq_neg_one_iff, eq_neg_one_iff', eq_neg_one_iff_not_one, eq_one_iff, eq_one_iff', eq_one_of_sq_sub_mul_sq_eq_zero, eq_one_of_sq_sub_mul_sq_eq_zero', eq_one_or_neg_one, eq_pow, eq_zero_iff, eq_zero_mod_of_eq_neg_one, hom_apply, mul, prime_dvd_of_eq_neg_one, sq_one, sq_one'	27
Total	29

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euler_criterion 📖	mathematical	—	IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	sq MulZeroClass.mul_zero euler_criterion_units
euler_criterion_units 📖	mathematical	—	Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField Monoid.toNatPow Units.instMonoid Units.instOne	—	instSubsingletonUnits NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' FiniteField.unit_isSquare_iff ringChar_zmod_n isSquare_iff_exists_sq card
exists_sq_eq_neg_one_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 AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' FiniteField.isSquare_neg_one_iff card
mod_four_ne_three_of_sq_eq_neg_one 📖	—	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	exists_sq_eq_neg_one_iff pow_two
mod_four_ne_three_of_sq_eq_neg_sq 📖	—	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	—	mod_four_ne_three_of_sq_eq_neg_sq' neg_eq_iff_eq_neg
mod_four_ne_three_of_sq_eq_neg_sq' 📖	—	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	—	mod_four_ne_three_of_sq_eq_neg_one one_pow div_self div_pow neg_div
pow_div_two_eq_neg_one_or_one 📖	mathematical	—	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Nat.Prime.eq_two_or_odd Fact.out Fintype.complete NeZero.one nontrivial Nat.Prime.one_lt' Nat.instAtLeastTwoHAddOfNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial one_pow neg_eq_self_mod_two mul_self_eq_one_iff IsDomain.to_noZeroDivisors instIsDomain pow_add two_mul Nat.two_mul_odd_div_two pow_card_sub_one_eq_one

(root)

Definitions

Name	Category	Theorems
legendreSym 📖	CompOp	31 math math: legendreSym.eq_neg_one_iff, legendreSym.eq_one_or_neg_one, legendreSym.mod, legendreSym.sq_one, jacobiSym.legendreSym.to_jacobiSym, legendreSym.eq_neg_one_iff_not_one, legendreSym.at_two, legendreSym.quadratic_reciprocity_three_mod_four, legendreSym.hom_apply, legendreSym.eq_one_iff, legendreSym.sq_one', legendreSym.quadratic_reciprocity', ZMod.gauss_lemma, legendreSym_mersenne_two, legendreSym.eq_zero_iff, Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym, legendreSym.at_zero, legendreSym.eq_one_iff', legendreSym.eq_pow, legendreSym.at_neg_one, legendreSym.card_sqrts, legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero', legendreSym.eq_neg_one_iff', legendreSym.at_neg_two, ZMod.eisenstein_lemma, legendreSym.mul, legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero, legendreSym.at_one, legendreSym_mersenne_three, legendreSym.quadratic_reciprocity, legendreSym.quadratic_reciprocity_one_mod_four

legendreSym

Definitions

Name	Category	Theorems
hom 📖	CompOp	1 math math: hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
at_neg_one 📖	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	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Int.cast_neg Int.cast_one quadraticChar_neg_one ZMod.ringChar_zmod_n ZMod.card
at_one 📖	mathematical	—	legendreSym	—	eq_1 Int.cast_one MulChar.map_one
at_zero 📖	mathematical	—	legendreSym	—	eq_1 Int.cast_zero MulChar.map_zero ZMod.nontrivial Nat.Prime.one_lt'
card_sqrts 📖	mathematical	—	Finset.card ZMod Set.toFinset setOf Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Subtype.fintype Set Set.instMembership Set.decidableSetOf ZMod.decidableEq ZMod.fintype NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' legendreSym	—	quadraticChar_card_sqrts NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.ringChar_zmod_n
eq_neg_one_iff 📖	mathematical	—	legendreSym IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField	—	quadraticChar_neg_one_iff_not_isSquare
eq_neg_one_iff' 📖	mathematical	—	legendreSym IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField	—	eq_neg_one_iff Int.cast_natCast
eq_neg_one_iff_not_one 📖	mathematical	—	legendreSym	—	quadraticChar_eq_neg_one_iff_not_one
eq_one_iff 📖	mathematical	—	legendreSym IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField	—	quadraticChar_one_iff_isSquare
eq_one_iff' 📖	mathematical	—	legendreSym IsSquare ZMod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField	—	eq_one_iff Nat.cast_zero Int.cast_zero Int.cast_natCast
eq_one_of_sq_sub_mul_sq_eq_zero 📖	mathematical	ZMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	legendreSym	—	eq_one_iff pow_two sub_eq_zero mul_one one_pow mul_inv_cancel₀ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Tactic.Ring.mul_one MulZeroClass.zero_mul
eq_one_of_sq_sub_mul_sq_eq_zero' 📖	mathematical	ZMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	legendreSym	—	eq_one_of_sq_sub_mul_sq_eq_zero sq_eq_zero_iff isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors ZMod.instIsDomain sub_zero MulZeroClass.mul_zero zero_pow two_ne_zero
eq_one_or_neg_one 📖	mathematical	—	legendreSym	—	quadraticChar_dichotomy
eq_pow 📖	mathematical	—	ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField legendreSym Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	eq_or_ne eq_1 quadraticChar_zero zero_pow LT.lt.ne' Nat.Prime.two_le Fact.out Nat.cast_zero Int.cast_zero ZMod.ringChar_zmod_n quadraticChar_eq_one_of_char_two Int.cast_one Fintype.complete NeZero.one ZMod.nontrivial Nat.Prime.one_lt' one_pow NeZero.of_gt' Nat.instCanonicallyOrderedAdd ZMod.card quadraticChar_eq_pow_of_char_ne_two'
eq_zero_iff 📖	mathematical	—	legendreSym ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	quadraticChar_eq_zero_iff
eq_zero_mod_of_eq_neg_one 📖	—	legendreSym ZMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddGroupWithOne.toIntCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	eq_zero_iff imp_iff_or_not one_ne_zero CharZero.eq_neg_self_iff IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.instCharZero eq_one_of_sq_sub_mul_sq_eq_zero' eq_one_of_sq_sub_mul_sq_eq_zero
hom_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Int.instSemiring MonoidWithZeroHom.funLike hom legendreSym	—	—
mul 📖	mathematical	—	legendreSym	—	Int.cast_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass
prime_dvd_of_eq_neg_one 📖	—	legendreSym Monoid.toNatPow Int.instMonoid	—	—	eq_zero_mod_of_eq_neg_one Int.cast_sub Int.cast_pow Int.cast_mul
sq_one 📖	mathematical	—	Monoid.toNatPow Int.instMonoid legendreSym	—	quadraticChar_sq_one
sq_one' 📖	mathematical	—	legendreSym Monoid.toNatPow Int.instMonoid	—	Int.cast_pow quadraticChar_sq_one'

---

← Back to Index