why \| is unexpected

Stream: new members

[klh]

image.png

[Patrick Massot]

You forgot to put a name.

[klh]

What is your meaning? What name?

[Patrick Massot]

A name for the assumption Lean is complaining about.

[Patrick Massot]

It would be a lot easier to help you if you post code instead of pictures (read #backticks for instructions).

[Patrick Massot]

I could have fixed your code, but I don’t want to type it because you posted an image.

[klh]

'''import mathlib

open Nat

variable(x y :ℕ+ ){n:ℕ+}

def a  : ℕ → ℕ

| 0 => 0

| 1 => 0

| n+2 => x * a (n + 1) + y * a n + 1

def a_n:=a n

def a_n₁:=a (n+1)

theorem  property (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hy: q∣y) :Nat.Coprime q (Nat.gcd a_p a_p₁) := by

sorry

theorem  property₁(p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hy: Corprime q y)(q∣a_p∧ q∣a_p₁):q>√p:= by

sorry'''

[Yaël Dillies]

Please read #backticks to learn how to format code on Zulip :smile:

[klh]

Thank you very much

[Yaël Dillies]

theorem  property₁(p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hy: q.Coprime y)(hq' : q∣a_p∧ q∣a_p₁):q>√p:= by
sorry

should work

[klh]

oh!I know.I made a stupid mistake . :clown:

[Notification Bot]

This topic was moved here from #lean4 > why \| is unexpected by Kyle Miller.