ZModChar

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

Statistics

Metric	Count
Definitions χ₄, χ₈, χ₈'	3
Theorems isQuadratic_χ₄, isQuadratic_χ₈, isQuadratic_χ₈', neg_one_pow_div_two_of_one_mod_four, neg_one_pow_div_two_of_three_mod_four, χ₄_apply, χ₄_eq_neg_one_pow, χ₄_int_eq_if_mod_four, χ₄_int_mod_four, χ₄_int_one_mod_four, χ₄_int_three_mod_four, χ₄_nat_eq_if_mod_four, χ₄_nat_mod_four, χ₄_nat_one_mod_four, χ₄_nat_three_mod_four, χ₈'_apply, χ₈'_eq_χ₄_mul_χ₈, χ₈'_int_eq_if_mod_eight, χ₈'_int_eq_χ₄_mul_χ₈, χ₈'_nat_eq_if_mod_eight, χ₈_apply, χ₈_int_eq_if_mod_eight, χ₈_int_mod_eight, χ₈_nat_eq_if_mod_eight, χ₈_nat_mod_eight	25
Total	28

ZMod

Definitions

Name	Category	Theorems
χ₄ 📖	CompOp	18 math math: χ₄_int_mod_four, χ₈'_int_eq_χ₄_mul_χ₈, χ₈'_eq_χ₄_mul_χ₈, χ₄_nat_one_mod_four, jacobiSym.neg, χ₄_int_three_mod_four, χ₄_nat_three_mod_four, χ₄_apply, χ₄_int_one_mod_four, χ₄_eq_neg_one_pow, legendreSym.at_neg_one, quadraticChar_odd_prime, χ₄_int_eq_if_mod_four, χ₄_nat_mod_four, quadraticChar_neg_one, jacobiSym.at_neg_one, isQuadratic_χ₄, χ₄_nat_eq_if_mod_four
χ₈ 📖	CompOp	12 math math: quadraticChar_two, χ₈'_int_eq_χ₄_mul_χ₈, χ₈'_eq_χ₄_mul_χ₈, legendreSym.at_two, χ₈_int_mod_eight, FiniteField.two_pow_card, isQuadratic_χ₈, χ₈_nat_mod_eight, jacobiSym.at_two, χ₈_nat_eq_if_mod_eight, χ₈_apply, χ₈_int_eq_if_mod_eight
χ₈' 📖	CompOp	9 math math: χ₈'_int_eq_if_mod_eight, χ₈'_nat_eq_if_mod_eight, χ₈'_int_eq_χ₄_mul_χ₈, χ₈'_eq_χ₄_mul_χ₈, jacobiSym.at_neg_two, quadraticChar_neg_two, isQuadratic_χ₈', χ₈'_apply, legendreSym.at_neg_two

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuadratic_χ₄ 📖	mathematical	—	MulChar.IsQuadratic ZMod CommRing.toCommMonoid commRing Int.instCommRing χ₄	—	—
isQuadratic_χ₈ 📖	mathematical	—	MulChar.IsQuadratic ZMod CommRing.toCommMonoid commRing Int.instCommRing χ₈	—	—
isQuadratic_χ₈' 📖	mathematical	—	MulChar.IsQuadratic ZMod CommRing.toCommMonoid commRing Int.instCommRing χ₈'	—	—
neg_one_pow_div_two_of_one_mod_four 📖	mathematical	—	Monoid.toNatPow Int.instMonoid	—	χ₄_nat_one_mod_four χ₄_eq_neg_one_pow Nat.odd_of_mod_four_eq_one
neg_one_pow_div_two_of_three_mod_four 📖	mathematical	—	Monoid.toNatPow Int.instMonoid	—	χ₄_nat_three_mod_four χ₄_eq_neg_one_pow Nat.odd_of_mod_four_eq_three
χ₄_apply 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄	—	—
χ₄_eq_neg_one_pow 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow Int.instMonoid	—	χ₄_nat_eq_if_mod_four mul_assoc add_comm Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid pow_add pow_mul neg_one_sq one_pow mul_one
χ₄_int_eq_if_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	intCast_mod Int.emod_lt_abs
χ₄_int_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	intCast_mod Nat.instAtLeastTwoHAddOfNat Nat.cast_ofNat
χ₄_int_one_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	χ₄_int_mod_four
χ₄_int_three_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	χ₄_int_mod_four
χ₄_nat_eq_if_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Nat.cast_zero Nat.cast_one Int.instCharZero Int.cast_natCast χ₄_int_eq_if_mod_four
χ₄_nat_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
χ₄_nat_one_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	χ₄_nat_mod_four
χ₄_nat_three_mod_four 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₄ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	χ₄_nat_mod_four
χ₈'_apply 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈'	—	—
χ₈'_eq_χ₄_mul_χ₈ 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈' χ₄ cast Ring.toAddGroupWithOne CommRing.toRing χ₈	—	—
χ₈'_int_eq_if_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈' AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	intCast_mod Int.emod_lt_abs
χ₈'_int_eq_χ₄_mul_χ₈ 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈' AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing χ₄ χ₈	—	cast_intCast charP χ₈'_eq_χ₄_mul_χ₈
χ₈'_nat_eq_if_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈' AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Nat.cast_zero Nat.cast_one Int.instCharZero Int.cast_natCast χ₈'_int_eq_if_mod_eight
χ₈_apply 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈	—	—
χ₈_int_eq_if_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	intCast_mod Int.emod_lt_abs
χ₈_int_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	intCast_mod Nat.instAtLeastTwoHAddOfNat Nat.cast_ofNat
χ₈_nat_eq_if_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Nat.cast_zero Nat.cast_one Int.instCharZero Int.cast_natCast χ₈_int_eq_if_mod_eight
χ₈_nat_mod_eight 📖	mathematical	—	DFunLike.coe MulChar ZMod CommRing.toCommMonoid commRing CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike χ₈ AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	natCast_mod

---

← Back to Index