## Stream: maths

### Topic: module

#### Johan Commelin (Nov 23 2018 at 12:49):

@Mario Carneiro Shouldn't this be flipped, for consistency with comp and llcomp?

def lcomp (f : M →ₗ N) : (N →ₗ P) →ₗ M →ₗ P := _ -- I would expect:   def lcomp (f : N →ₗ P) : (M →ₗ N) →ₗ M →ₗ P :=


#### Mario Carneiro (Nov 23 2018 at 12:50):

maybe, but the other direction is harder

#### Mario Carneiro (Nov 23 2018 at 12:50):

there is an order to the definitions

#### Johan Commelin (Nov 23 2018 at 12:50):

Also, are there compatibilities between comp and lcomp etc...? Is (lcomp f).to_fun defeq to f.comp?

#### Mario Carneiro (Nov 23 2018 at 12:50):

yeah, it's all defeq

#### Mario Carneiro (Nov 23 2018 at 12:50):

it's just composition so it's easy

#### Mario Carneiro (Nov 23 2018 at 12:52):

also there is a difference between lcomp that is there and the one you said

#### Mario Carneiro (Nov 23 2018 at 12:52):

one is precomposition and the other is postcomposition

#### Johan Commelin (Nov 23 2018 at 13:07):

Right, and I think the library isn't completely consistent about which one it uses for comp, lcomp and llcomp. Wouldn't it be easier if they were all post-composition?

#### Mario Carneiro (Nov 23 2018 at 13:09):

I mean there is a need for it, I didn't write that for no reason

#### Mario Carneiro (Nov 23 2018 at 13:09):

it's used before we have tensor products and swap and eval and such, so they aren't yet interchangeable

Ok, I see

#### Johan Commelin (Nov 23 2018 at 13:10):

So, may I then complain that the name is slightly confusing?

#### Mario Carneiro (Nov 23 2018 at 13:10):

rcomp :)

#### Johan Commelin (Nov 23 2018 at 17:23):

@Mario Carneiro I couldn't find where the zero linear map is defined, but apparently it is somewhere. However ⇑0 m doesn't simp to 0. Where should I add this simp rule?

Last updated: May 09 2021 at 09:11 UTC