Commit 2024-05-10 15:40 c49b5e16

View on Github →

feat: add Equiv.prodSubtypeFstEquivSubtypeProd (#12802) See Zulip

Estimated changes

Modified Mathlib/Logic/Equiv/Basic.lean

added def Equiv.prodSubtypeFstEquivSubtypeProd