collaborators

1 paper

math.CT2026

Unbiasing symmetric monoidal categories in Lean

Robin Carlier

We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by exte…