# Zulip Chat Archive

## Stream: new members

### Topic: Accessing properties of list elements while mapping them

#### Michael Stoll (Mar 13 2022 at 21:12):

I'm a bit stuck with the following problem. I want to convert the list of prime factors of a nonzero natural number a, `a.factors : list ℕ`

, into a list of primes, say `prime_factors a : list nat.primes`

. The obvious way to do this seems to be to use `list.map`

to convert the elements from type `ℕ`

to type `nat.primes`

:

```
list.map (λ p, ⟨p, _⟩) a.factors
```

Now the underscore needs to be a proof of the fact that `p`

is a prime. I know that `p`

is a prime, from

```
((nat.mem_factors ha).mp _).left
```

where `ha : a ≠ 0`

and the underscore is a proof of `p ∈ a.factors`

.

Now my question is, how I can introduce this knowledge into the function I want to use in `list.map`

above?

#### Michael Stoll (Mar 13 2022 at 21:24):

Or maybe a different approach should be used?

#### Jakub Kądziołka (Mar 13 2022 at 21:30):

I think you need to find, or write, a function like `map`

that gives you this as an assumption

#### Alex J. Best (Mar 13 2022 at 21:42):

Michael Stoll said:

Or maybe a different approach should be used?

I'm curious what you need a list of dosc#nat.primes for, its not used so much, people instead just tend to use docs#nat.prime_of_mem_factors when needed

#### Michael Stoll (Mar 13 2022 at 21:53):

OK, maybe this is an XY problem. What I really would like to have is something like

```
def prime_factors_as_finset_of_primes (a : ℤ) : finset nat.primes := ...
```

that gives me the prime factors of `a`

as a `finset`

. The idea was to first convert the `list`

of factors to a list of primes and then to turn the `list`

into a `finset`

.

#### Michael Stoll (Mar 13 2022 at 21:54):

But in any case, there *should* be a reasonable way of changing the type of the list elements to a subtype if we know that all the elements satisfy the relevant property?

Last updated: Dec 20 2023 at 11:08 UTC