# IRC log for #isabelle, 2017-04-28

All times shown according to UTC.

Time Nick Message
01:49 ilbot3 joined #isabelle
01:49 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
08:05 dave24 joined #isabelle
11:42 ertes joined #isabelle
12:20 int-e pruvisto: fwiw, the link to the Totient theory worked for me (and I'm not logged into bitbucket atm).
12:30 pruvisto int-e: yes I changed the visibility by now
12:30 pruvisto it was set to "private" at first for some reason
12:30 pruvisto I switched it to "public" then but it still didn't work
12:30 int-e ah.
12:30 pruvisto but after an hour or so, it finally worked
12:30 pruvisto apparently there's a bit of a delay there
12:30 int-e gotta love caching
12:47 dmiles joined #isabelle
12:49 dmiles joined #isabelle
15:57 ertes joined #isabelle
22:05 chindy i should probably have paid more attention in linear algebra, but does this lemma hold? lemma  "(P::real^2) > 0 ⟹ P ∙ A > P ∙ B ⟹ A > B"
22:06 int-e well, what if all entries in P are equal
22:07 int-e actually, hmm
22:07 chindy what then ?
22:07 int-e what's ∙ here?
22:07 chindy dot product
22:08 int-e okay then. let's pick P = (1,1), A = (2,0), B = (0,1)
22:09 chindy ah... im an idiot
22:09 chindy :P
22:10 int-e let me guess, > is not a total order :)
22:10 chindy yea
22:22 chindy int-e: what about  ∃i . A$i > B$i instead of A > B ?
22:37 ertes joined #isabelle
22:43 int-e well, that's the negation of !i. A$i <= B$i, and A <= B and P > 0 implies P \cdot A <= P \cdot B... so that should work fine.