Stream: new members

Topic: Product of functions defined on groups

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⟩


?

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

Jalex Stark (Jun 20 2020 at 16:20):

Nicolò Cavalleri said:

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

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


work for you?

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

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


work for you?

Yes it does!

Jalex Stark (Jun 20 2020 at 16:24):

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

Jalex Stark (Jun 20 2020 at 16:25):

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

Nicolò Cavalleri (Jun 20 2020 at 16:28):

Should I write suggest instead of apply_instance?

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,

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

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.

Nicolò Cavalleri (Jun 20 2020 at 16:34):

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

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


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