Type mismatch at application

Stream: new members

[Bolton Bailey]

Here is my MWE

import data.zmod.basic

theorem lucas_primality (p : ℕ) (a : zmod p)
  (ha : a^(p-1) = 1)
  (hd : (∀ d : ℕ, (prime d) ∧ (d | (p-1)) -> a^d ≠ 1))
  : p.prime :=
begin
  sorry,
end

I get the error

type mismatch at application
  prime d ∧ d
term
  d
has type
  ℕ
but is expected to have type
  Prop

I've counted my parentheses a few times now. I don't understand how it is possible for the error mismatch to parse out the expression prime d ∧ d when the parentheses tell it not to read it that way. Why am I getting this error?

[Floris van Doorn]

I expect you need to replace | by \|

[Bolton Bailey]

Thank you

[Bolton Bailey]

Also, I would like to respectfully register my disagreement with the design decision that | should be interpreted differently by lean from \|.

[Mario Carneiro]

this is a necessary evil because | is used as a keyword in a few positions, e.g. to separate the arms of a pattern matching definition or inductive type

[Mario Carneiro]

personally I would have gone for a visually more distinct symbol for divides like ∥

[Floris van Doorn]

That is a fair criticism. Unfortunately | has a few important built-in meanings in Lean, and it's hard (read: impossible without modifying the source code) to overload that notation to also mean divisibility.
The same could be said about LaTeX, and at least the LaTeX input \mid also gives this symbol in Lean.

[Mario Carneiro]

although people routinely get it wrong in latex

[Eric Rodriguez]

Bolton Bailey said:

Here is my MWE

import data.zmod.basic

theorem lucas_primality (p : ℕ) (a : zmod p)
  (ha : a^(p-1) = 1)
  (hd : (∀ d : ℕ, (prime d) ∧ (d | (p-1)) -> a^d ≠ 1))
  : p.prime :=
begin
  sorry,
end

I get the error

type mismatch at application
  prime d ∧ d
term
  d
has type
  ℕ
but is expected to have type
  Prop

I've counted my parentheses a few times now. I don't understand how it is possible for the error mismatch to parse out the expression prime d ∧ d when the parentheses tell it not to read it that way. Why am I getting this error?

I think lucas lehmer is done somewhere in mathlib as a verified algo, fwiw

[Bolton Bailey]

Not doing Lucas-Lehmer, which I understand is for Mersenne primes. I want to do the test linked here

[Johan Commelin]

@Bolton Bailey Lucas Lehmer is already in mathlib. But I guess you already knew that.