Zulip Chat Archive

Stream: new members

Topic: Product of functions defined on groups


view this post on Zulip Nicolò Cavalleri (Jun 20 2020 at 16:14):

Does the standard libary already contain anything like:

import geometry.manifold.real_instances
import algebra.group.defs

 def maps_mul {A : Type*} {G : Type*} [group G] (f : A  G) (g : A  G) : (A  G) := λ a : A, f a * g a

 instance mul_maps {A : Type*} {G : Type*} [group G] : has_mul (A  G) := maps_mul

?

view this post on Zulip Nicolò Cavalleri (Jun 20 2020 at 16:17):

I mean Lean does not say writing f*g is wrong but also does not find the definition for me

view this post on Zulip Jalex Stark (Jun 20 2020 at 16:20):

Nicolò Cavalleri said:

I mean Lean does not say writing f*g is wrong

what are your imports? does

instance mul_maps
{A : Type*} {G : Type*} [group G] :
has_mul (A  G) := by apply_instance

work for you?

view this post on Zulip Nicolò Cavalleri (Jun 20 2020 at 16:22):

Jalex Stark said:

Nicolò Cavalleri said:

I mean Lean does not say writing f*g is wrong

what are your imports? does

instance mul_maps
{A : Type*} {G : Type*} [group G] :
has_mul (A  G) := by apply_instance

work for you?

Yes it does!

view this post on Zulip Jalex Stark (Jun 20 2020 at 16:24):

including your imports is really important to get help on questions like this

view this post on Zulip Jalex Stark (Jun 20 2020 at 16:25):

did apply_instance tell you the name you were looking for? if not, does suggest?

view this post on Zulip Nicolò Cavalleri (Jun 20 2020 at 16:28):

Should I write suggest instead of apply_instance?

view this post on Zulip Jalex Stark (Jun 20 2020 at 16:30):

my understanding is that suggest is in an interactive tactic which finds stuff that looks like your goal and tells them to you in a list,

view this post on Zulip Jalex Stark (Jun 20 2020 at 16:30):

while apply_instance will close goals using typeclass inference, but won't tell you what it found

view this post on Zulip Sebastien Gouezel (Jun 20 2020 at 16:31):

def  foo
{A : Type*} {G : Type*} [group G] :
has_mul (A  G) := by apply_instance

#print foo

will tell you where the instance is coming from.

view this post on Zulip Nicolò Cavalleri (Jun 20 2020 at 16:34):

Great thanks! It looks to be a general definition for all algebraic structures

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 16:39):

Mario suggested this pattern recently, which is a little shorter:

import algebra.pi_instances

variables {A : Type*} {G : Type*} [group G]
#check (by apply_instance : has_mul (A  G))

view this post on Zulip Sebastien Gouezel (Jun 20 2020 at 16:50):

Definitely shorter, but definitely more magical and harder to remember :)


Last updated: May 10 2021 at 00:31 UTC