LucasPrimality

📁 Source: Mathlib/NumberTheory/LucasPrimality.lean

Statistics

Metric	Count
Definitions	0
Theorems lucas_primality, lucas_primality_iff, reverse_lucas_primality	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lucas_primality 📖	mathematical	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Nat.Prime	—	Nat.prime_two dvd_zero pow_zero Nat.prime_iff_card_units LE.le.antisymm Nat.card_units_zmod_lt_sub_one instIsDedekindFiniteMonoid pow_succ' tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le orderOf_eq_of_pow_and_pow_div_prime tsub_pos_of_lt orderOf_injective Units.val_injective orderOf_le_card_univ
lucas_primality_iff 📖	mathematical	—	Nat.Prime ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	reverse_lucas_primality lucas_primality
reverse_lucas_primality 📖	mathematical	Nat.Prime	ZMod Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsCyclic.exists_generator instIsCyclicUnitsOfFinite ZMod.instIsDomain instFiniteUnits Finite.of_fintype NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' orderOf_eq_card_of_forall_mem_zpowers Nat.card_eq_fintype_card Nat.prime_iff_card_units tsub_pos_iff_lt Nat.instOrderedSub Nat.Prime.one_lt orderOf_eq_iff orderOf_injective Units.val_injective LT.lt.trans zero_lt_one Nat.instZeroLEOneClass

---

← Back to Index