Theorem Prod.toSigma_injective

Modification history

2025-08-20 19:33
Mathlib/Data/Sigma/Basic.lean
feat: Cantor normal form as a finitely supported function (#28586)
Added Prod.toSigma_injectiveView on Github →