Theorem Equiv.prodComm_trans_uniqueProd

Modification history

2026-11-03 04:18
Mathlib/Logic/Equiv/Prod.lean
feat(Order): `OrderIso.prodCongr` (#45251) …
Added Equiv.prodComm_trans_uniqueProdView on Github →