## 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