the prime factorization of `n`

Stream: new members

[Nga Ngo]

I don't understand this codes in Lean Library (data nat prime.lean -line 233-239)
/-- factors n is the prime factorization of n, listed in increasing order. -/
def factors : ℕ → list ℕ
| 0 := []
| 1 := []
| n@(k+2) :=
let m := min_fac n in have n / m < n := factors_lemma,
m :: factors (n / m)

What is n@(k+2) ?
Could someone explain for me? Thanks.

[Mario Carneiro]

It's a pattern match, so we are in the case where n = k+2. The n@notation allows us to also give a name to k+2, the original argument of the function; you can replace n with k+2 everywhere and it would be the same

[Mii Nguyen]

@Mario Carneiro what does it mean in havein the loop?

[Mario Carneiro]

it's two statements:

let m := min_fac n in
have n / m < n, from factors_lemma,
m :: factors (n / m)