# Zulip Chat Archive

## Stream: new members

### Topic: contradiction

#### 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