mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

Published 20 hours ago • verified publisher icon avigad

switch proposition names `pge` and `primep` in S01_Sets.lean

Open yannickseurin opened this issue 8 months ago • 0 comments

Names of propositions pge and primep don't match when destructing Nat.exists_infinite_primes

yannickseurin avatar Jun 21 '24 07:06 yannickseurin