Zulip Chat Archive

Stream: new members

Topic: contradiction


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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