# Zulip Chat Archive

## Stream: new members

### Topic: definition with conditions

#### Ashwin Iyengar (Feb 11 2021 at 17:09):

Here's a question (don't take the context too seriously). Let's say I have

```
def a (R : Type) [ring R] := ℕ → R
```

so an "a" is a sequence of elements of R. I then want to define "b", which should be an "a", but such that the nth element of the sequence is equal to the zero element of the ring if n > 3. What's the best way to write this definition? I somehow want to package the data of the sequence, and a proof of vanishing for n > 3 into one definition.

#### Eric Wieser (Feb 11 2021 at 17:11):

One definition would be`{f : a R // ∀ n, 3 < n → f n = 0}`

#### Kyle Miller (Feb 11 2021 at 17:17):

Sometimes structures are nice:

```
structure b (R : Type*) [ring R] :=
(a : ℕ → R)
(property : ∀ n, 3 < n → a n = 0)
```

(This doesn't define an `a`

type. I don't know the context, but `ℕ → R`

is a simple enough type that it might not need to be called anything but itself.)

#### Ashwin Iyengar (Feb 11 2021 at 17:19):

Thanks, I'll try working with a structure. In my context `a`

is actually `mv_power_series`

(multivariable power series) and I'm trying to put some conditions on the coefficients.

#### Kyle Miller (Feb 11 2021 at 17:20):

If there's only one property, @Eric Wieser's suggestion of a `subtype`

is good, too, especially since there are a number of lemmas surrounding them.

#### Kevin Buzzard (Feb 11 2021 at 17:21):

@Ashwin Iyengar why aren't you at my course!! It's running until 6

#### Ashwin Iyengar (Feb 11 2021 at 17:22):

Oh! How do I join?

Last updated: May 14 2021 at 22:15 UTC