Zulip Chat Archive

Stream: new members

Topic: Implicit argument inclusion

Frédéric Dupuis (Sep 04 2020 at 14:57):

I'm trying to write the following lemma:

variables {α K : Type*}
  [nondiscrete_normed_field K] [algebra  K] [is_R_or_C K]
  [inner_product_space K α]

lemma parallelogram_law_with_norm {x y : α} :
  x + y * x + y + x - y * x - y = 2 * (x * x + y * y) := sorry

The problem is that the norm comes from the inner product, but K never shows up in the lemma statement, which means that Lean never finds the relevant has_norm instance. Is there any way to feed that information in manually?

Frédéric Dupuis (Sep 04 2020 at 15:07):

The reason I'm hoping there's a way to do this without just recopying all the implicit arguments manually is that I have also defined lots of notation for that inner product that I would like to be available here.

Ruben Van de Velde (Sep 04 2020 at 15:39):

Is this what include K is for?

Kenny Lau (Sep 04 2020 at 15:43):


Frédéric Dupuis (Sep 04 2020 at 16:00):

Thanks! Is there also a way to also stop the inclusion after this lemma?

Bryan Gin-ge Chen (Sep 04 2020 at 16:02):

omit K

Scott Morrison (Sep 05 2020 at 01:52):

Alternatively, you can just embed the include within a section ... end; it only lasts for that scope. This has the added bonus that sections are helpful for the reader anyway, while omit adds a burden of keeping track of more things.

Last updated: Dec 20 2023 at 11:08 UTC