GodelBetaFunction

📁 Source: Mathlib/Logic/Godel/GodelBetaFunction.lean

Statistics

Metric	Count
Definitions beta, unbeta	2
Theorems beta_unbeta_coe, coprime_mul_succ, coprimes_lt	3
Total	5

Nat

Definitions

Name	Category	Theorems
beta 📖	CompOp	1 math math: beta_unbeta_coe
unbeta 📖	CompOp	1 math math: beta_unbeta_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
beta_unbeta_coe 📖	mathematical	—	beta unbeta	—	unpair_pair mod_eq_of_modEq IsDomain.to_noZeroDivisors instIsDomain Finset.coe_univ Set.pairwise_univ Subtype.prop coprimes_lt
coprime_mul_succ 📖	—	—	—	—	coprime_of_dvd Prime.dvd_mul Prime.ne_one Dvd.dvd.mul_left
coprimes_lt 📖	—	—	—	—	le_max_of_le_right Finset.le_sup le_trans self_le_factorial lt_of_lt_of_le

---

← Back to Index