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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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 Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd 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.toPow 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.toPow 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.toPow 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.toPow 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 📖	mathematical	legendreSym ZMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing ZMod.instField Monoid.toPow 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	ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	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.toPow Int.instMonoid	—	—	eq_zero_mod_of_eq_neg_one Int.cast_sub Int.cast_pow Int.cast_mul
sq_one 📖	mathematical	—	Monoid.toPow Int.instMonoid legendreSym	—	quadraticChar_sq_one
sq_one' 📖	mathematical	—	legendreSym Monoid.toPow Int.instMonoid	—	Int.cast_pow quadraticChar_sq_one'

---

← Back to Index