mathlib

015bb41a - monoidal structure from equivalence of category partially finished