contradiction

Stream: new members

[Debendro Mookerjee]

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]

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]

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]

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.