Stream: new members

Debendro Mookerjee (Feb 12 2020 at 16:37):

theorem square_root_prime(n : ℕ)(pc: ∀ p : ℕ, prime p ∧ dvd p n ∧ p*p > n) : prime n :=
begin
absurd,
end

How do I negate the statement prime p?

Kevin Buzzard (Feb 12 2020 at 16:43):

I don't quite know what you're doing, but you are assuming a hypothesis pc which is false so you should be able to prove anything. You're assuming that every number p is prime, and also divides n, and also has square bigger than n.

Kevin Buzzard (Feb 12 2020 at 16:44):

Also I can't get your code to compile -- are there missing imports / opens etc? There is more than one definition of prime in mathlib (corresponding to the fact that there is more than one usage of the word in mathematics)

Kevin Buzzard (Feb 12 2020 at 16:48):

absurd is a function; it takes proofs of P and not P, and spits out a term of any type you like. Within a begin end block you have to use tactics.

Last updated: May 14 2021 at 00:42 UTC