Constructive tensor product

Stream: maths

[Kenny Lau]

https://github.com/kckennylau/Lean/blob/master/constructive_tensor_product.lean

[Kenny Lau]

I built a constructive tensor product and proved that it is a module. I have not proved its properties.

[Kenny Lau]

But inside there is also a constructive version of free abelian group

[Kevin Buzzard]

I needed free abelian group on a type and the finsupp approach demanded I had decidable equality on the type. Is this to be expected?

[Kenny Lau]

my version does not need decidable equality

[Kenny Lau]

but finsupp does need decidable equality

[Kevin Buzzard]

Oh great! I was a bit confused as to why I suddenly needed it.

[Kenny Lau]

https://github.com/kckennylau/Lean/blob/master/constructive_tensor_product.lean

[Kenny Lau]

I proved the property

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

So now back to alg closure? ;-)

[Kenny Lau]

hmm

[Kenny Lau]

let's prove the separability lemma first