Theorem Prod.toSigma_inj

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_injView on Github →