definition with conditions

Stream: new members

[Ashwin Iyengar]

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]

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

[Kyle Miller]

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]

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]

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]

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

[Ashwin Iyengar]

Oh! How do I join?