module

Stream: maths

[Johan Commelin]

@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]

maybe, but the other direction is harder

[Mario Carneiro]

there is an order to the definitions

[Johan Commelin]

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

[Mario Carneiro]

yeah, it's all defeq

[Mario Carneiro]

it's just composition so it's easy

[Mario Carneiro]

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

[Mario Carneiro]

one is precomposition and the other is postcomposition

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Ok, I see

[Johan Commelin]

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

[Mario Carneiro]

rcomp :)

[Johan Commelin]

@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?