PrimesCongruentOne

📁 Source: Mathlib/NumberTheory/PrimesCongruentOne.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_prime_gt_modEq_one, frequently_atTop_modEq_one, infinite_setOf_prime_modEq_one	3
Total	3

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_prime_gt_modEq_one 📖	mathematical	—	Prime ModEq	—	LE.le.eq_or_lt exists_infinite_primes modEq_one le_iff_exists_add' instCanonicallyOrderedAdd LT.lt.le le_mul_of_le_of_one_le instMulLeftMono factorial_pos le_tsub_of_add_le_left instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Polynomial.sub_one_lt_natAbs_cyclotomic_eval LT.lt.ne' minFac_prime Int.cast_natCast map_natCast RingHom.instRingHomClass Polynomial.IsRoot.def Polynomial.map_cyclotomic_int Polynomial.eval_map coe_castRingHom Polynomial.eval₂_hom Int.coe_castRingHom ZMod.intCast_zmod_eq_zero_iff_dvd minFac_dvd Prime.coprime_iff_not_dvd Fact.out Polynomial.coprime_of_root_cyclotomic Ne.bot_lt not_le dvd_mul_of_dvd_right dvd_factorial minFac_pos ZMod.orderOf_dvd_card_sub_one CharP.cast_eq_zero_iff ZMod.charP IsPrimitiveRoot.eq_orderOf Polynomial.isRoot_cyclotomic_iff ZMod.instIsDomain NeZero.of_not_dvd dvd_mul_of_dvd_left ModEq.symm modEq_iff_dvd' Prime.pos
frequently_atTop_modEq_one 📖	mathematical	—	Filter.Frequently Prime ModEq Filter.atTop instPreorder	—	Filter.frequently_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instArchimedeanNat exists_prime_gt_modEq_one LT.lt.le
infinite_setOf_prime_modEq_one 📖	mathematical	—	Set.Infinite setOf Prime ModEq	—	frequently_atTop_iff_infinite frequently_atTop_modEq_one

---

← Back to Index