Theorem Nat.Prime.one_le

Modification history

2024-01-30 09:46
Mathlib/Data/Nat/Prime.lean
feat(Data/Nat/Prime): some lemmas on primes and powers (#10025) …
Added Nat.Prime.one_leView on Github →