Basic

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

Statistics

Metric	Count
Definitions quadraticChar, quadraticCharFun	2
Theorems isSquare_neg_one_iff, quadraticCharFun_eq_one_of_char_two, quadraticCharFun_eq_pow_of_char_ne_two, quadraticCharFun_eq_zero_iff, quadraticCharFun_mul, quadraticCharFun_one, quadraticCharFun_zero, quadraticChar_apply, quadraticChar_card_sqrts, quadraticChar_dichotomy, quadraticChar_eq_neg_one_iff_not_one, quadraticChar_eq_one_of_char_two, quadraticChar_eq_pow_of_char_ne_two, quadraticChar_eq_pow_of_char_ne_two', quadraticChar_eq_zero_iff, quadraticChar_exists_neg_one, quadraticChar_exists_neg_one', quadraticChar_isQuadratic, quadraticChar_ne_one, quadraticChar_neg_one, quadraticChar_neg_one_iff_not_isSquare, quadraticChar_one_iff_isSquare, quadraticChar_sq_one, quadraticChar_sq_one', quadraticChar_sum_zero, quadraticChar_zero	26
Total	28

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSquare_neg_one_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 AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	isSquare_of_char_two Finite.of_fintype one_ne_zero Nat.odd_of_mod_four_eq_three even_card_of_char_two odd_card_of_char_ne_two quadraticChar_one_iff_isSquare neg_ne_zero one_ne_zero' NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing quadraticChar_neg_one ZMod.χ₄_nat_eq_if_mod_four

(root)

Definitions

Name	Category	Theorems
quadraticChar 📖	CompOp	22 math math: quadraticChar_card_sqrts, quadraticChar_card_card, quadraticChar_two, quadraticChar_isQuadratic, quadraticChar_dichotomy, quadraticChar_sum_zero, quadraticChar_eq_zero_iff, quadraticChar_zero, quadraticChar_exists_neg_one', quadraticChar_neg_two, quadraticChar_eq_one_of_char_two, quadraticChar_sq_one, quadraticChar_odd_prime, quadraticChar_sq_one', quadraticChar_apply, quadraticChar_neg_one_iff_not_isSquare, quadraticChar_eq_pow_of_char_ne_two, quadraticChar_eq_pow_of_char_ne_two', quadraticChar_neg_one, quadraticChar_eq_neg_one_iff_not_one, quadraticChar_one_iff_isSquare, quadraticChar_exists_neg_one
quadraticCharFun 📖	CompOp	7 math math: quadraticCharFun_eq_zero_iff, quadraticCharFun_eq_one_of_char_two, quadraticCharFun_one, quadraticCharFun_mul, quadraticCharFun_eq_pow_of_char_ne_two, quadraticChar_apply, quadraticCharFun_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quadraticCharFun_eq_one_of_char_two 📖	mathematical	ringChar Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	quadraticCharFun Semiring.toMonoidWithZero Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	FiniteField.isSquare_of_char_two Finite.of_fintype
quadraticCharFun_eq_pow_of_char_ne_two 📖	mathematical	—	quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow MonoidWithZero.toMonoid Fintype.card AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	FiniteField.isSquare_iff
quadraticCharFun_eq_zero_iff 📖	mathematical	—	quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
quadraticCharFun_mul 📖	mathematical	—	quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	MulZeroClass.zero_mul quadraticCharFun_zero MulZeroClass.mul_zero mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain quadraticCharFun_eq_one_of_char_two mul_one quadraticCharFun_eq_pow_of_char_ne_two mul_pow FiniteField.pow_dichotomy Ring.neg_one_ne_one_of_char_ne_two IsLocalRing.toNontrivial Field.instIsLocalRing mul_neg neg_neg
quadraticCharFun_one 📖	mathematical	—	quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing
quadraticCharFun_zero 📖	mathematical	—	quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
quadraticChar_apply 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar quadraticCharFun Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.IsSquare.decidablePred Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
quadraticChar_card_sqrts 📖	mathematical	—	Finset.card Set.toFinset setOf Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subtype.fintype Set Set.instMembership Set.decidableSetOf DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	Set.toFinset_congr isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Set.toFinset_card MulChar.map_zero IsLocalRing.toNontrivial Field.instIsLocalRing quadraticChar_one_iff_isSquare Finset.ext Set.toFinset_setOf pow_two List.toFinset_cons Finset.instLawfulSingleton sq_eq_sq_iff_eq_or_eq_neg Nat.cast_one Int.instCharZero List.toFinset_nil Finset.card_pair Ring.eq_self_iff_eq_zero_of_char_ne_two mul_self_eq_zero quadraticChar_neg_one_iff_not_isSquare neg_add_cancel Finset.filter.congr_simp
quadraticChar_dichotomy 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE quadraticChar_sq_one
quadraticChar_eq_neg_one_iff_not_one 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	quadraticChar_dichotomy
quadraticChar_eq_one_of_char_two 📖	mathematical	ringChar Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	quadraticCharFun_eq_one_of_char_two
quadraticChar_eq_pow_of_char_ne_two 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.card AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	quadraticCharFun_eq_pow_of_char_ne_two
quadraticChar_eq_pow_of_char_ne_two' 📖	mathematical	—	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.card	—	Fintype.one_lt_card IsLocalRing.toNontrivial Field.instIsLocalRing two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid quadraticCharFun_zero Int.cast_zero zero_pow LT.lt.ne' quadraticChar_eq_pow_of_char_ne_two Int.cast_one FiniteField.pow_dichotomy Int.cast_ite Int.cast_neg
quadraticChar_eq_zero_iff 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	quadraticCharFun_eq_zero_iff
quadraticChar_exists_neg_one 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	quadraticChar_neg_one_iff_not_isSquare FiniteField.exists_nonsquare Finite.of_fintype
quadraticChar_exists_neg_one' 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Mathlib.Tactic.Contrapose.contrapose₁ ne_of_eq_of_ne MulChar.map_nonunit zero_eq_neg one_ne_zero quadraticChar_exists_neg_one
quadraticChar_isQuadratic 📖	mathematical	—	MulChar.IsQuadratic CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Int.instCommRing quadraticChar	—	quadraticChar_zero quadraticChar_dichotomy
quadraticChar_ne_one 📖	—	—	—	—	quadraticChar_exists_neg_one' MulChar.one_apply Units.isUnit
quadraticChar_neg_one 📖	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 AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ZMod ZMod.commRing ZMod.χ₄ AddMonoidWithOne.toNatCast CommRing.toRing Fintype.card	—	quadraticChar_eq_pow_of_char_ne_two neg_ne_zero one_ne_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing ZMod.χ₄_eq_neg_one_pow FiniteField.odd_card_of_char_ne_two Nat.even_or_odd Even.neg_one_pow Odd.neg_one_pow Ring.neg_one_ne_one_of_char_ne_two
quadraticChar_neg_one_iff_not_isSquare 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MulChar.map_zero IsLocalRing.toNontrivial Field.instIsLocalRing quadraticChar_eq_neg_one_iff_not_one quadraticChar_one_iff_isSquare
quadraticChar_one_iff_isSquare 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
quadraticChar_sq_one 📖	mathematical	—	Monoid.toNatPow Int.instMonoid DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	pow_two map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass quadraticChar_sq_one'
quadraticChar_sq_one' 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
quadraticChar_sum_zero 📖	mathematical	—	Finset.sum Int.instAddCommMonoid Finset.univ DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar	—	MulChar.sum_eq_zero_of_ne_one Int.instIsDomain quadraticChar_ne_one
quadraticChar_zero 📖	mathematical	—	DFunLike.coe MulChar CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike quadraticChar MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	quadraticCharFun_zero

---

← Back to Index