Zulip Chat Archive

Stream: general

Topic: Trouble feeding instances


view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 19:53):

In order.filter.filter_product, I'm trying to write:

@[simp] lemma of_div [division_ring β] (U : is_ultrafilter φ) (x y : β) :
  of (x / y) = (@division_ring_has_div β* (filter_product.division_ring U) (filter_product.division_ring U)).div
   (of x) (of y : β*) := sorry

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 19:54):

(to try and bypass the problem of U not being an instance)

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 19:54):

But Lean gives weird errors:

invalid field notation, function 'has_div.div' does not have explicit argument with type (has_div ...)

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 19:55):

Which doesn't seem to make sense, as trying to access a field has_div out of has_div.div is certainly not what I'm doing.

view this post on Zulip Chris Hughes (Mar 26 2019 at 19:57):

In order to use the dot notation, you need the has_div argument to has_div.div to be explicit.

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 19:59):

Oh, right -- of course.

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 26 2019 at 20:00):

Yes, this works.

@[simp] lemma of_div [division_ring β] (U : is_ultrafilter φ) (x y : β) :
  of (x / y) = @has_div.div _ (@division_ring_has_div β* (filter_product.division_ring U) (filter_product.division_ring U))
  (of x) (of y : β*)

Last updated: May 06 2021 at 21:09 UTC