QuadraticReciprocity

📁 Source: Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

Statistics

Metric	Count
Definitions	0
Theorems mod_four_eq_three_of_nat_prime_of_prime, prime_iff_mod_four_eq_three_of_nat_prime, prime_of_nat_prime_of_mod_four_eq_three	3
Total	3

GaussianInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mod_four_eq_three_of_nat_prime_of_prime 📖	—	Prime GaussianInt CommSemiring.toCommMonoidWithZero Zsqrtd.instCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.addGroupWithOne	—	—	Nat.Prime.eq_two_or_odd Fact.out Irreducible.isUnit_or_isUnit Prime.irreducible IsDomain.toIsCancelMulZero EuclideanDomain.instIsDomain Nat.instAtLeastTwoHAddOfNat mul_one mul_neg neg_neg neg_add_cancel sub_neg_eq_add Nat.instCharZero by_contradiction ZMod.exists_sq_eq_neg_one_iff ZMod.val_lt NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.natCast_zmod_val pow_two CharP.cast_eq_zero_iff ZMod.charP Nat.cast_add Nat.cast_mul Nat.cast_one Zsqrtd.ext sq MulZeroClass.mul_zero add_zero MulZeroClass.zero_mul one_mul Nat.cast_zero NeZero.one ZMod.nontrivial mul_lt_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono lt_irrefl sub_zero add_comm norm_le_norm_mul_left Nat.cast_pow
prime_iff_mod_four_eq_three_of_nat_prime 📖	mathematical	—	Prime GaussianInt CommSemiring.toCommMonoidWithZero Zsqrtd.instCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.addGroupWithOne	—	mod_four_eq_three_of_nat_prime_of_prime prime_of_nat_prime_of_mod_four_eq_three
prime_of_nat_prime_of_mod_four_eq_three 📖	mathematical	—	Prime GaussianInt CommSemiring.toCommMonoidWithZero Zsqrtd.instCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.addGroupWithOne	—	irreducible_iff_prime IsDomain.toIsCancelMulZero EuclideanDomain.instIsDomain UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain by_contradiction sq_add_sq_of_nat_prime_of_not_irreducible ZMod.natCast_mod Nat.cast_add Nat.cast_pow

---

← Back to Index