Product of functions defined on groups

Stream: new members

[Nicolò Cavalleri]

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⟩

?

[Nicolò Cavalleri]

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

[Jalex Stark]

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?

[Nicolò Cavalleri]

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!

[Jalex Stark]

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

[Jalex Stark]

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

[Nicolò Cavalleri]

Should I write suggest instead of apply_instance?

[Jalex Stark]

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,

[Jalex Stark]

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

[Sebastien Gouezel]

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.

[Nicolò Cavalleri]

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

[Bryan Gin-ge Chen]

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

[Sebastien Gouezel]

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