Commit 2023-07-17 08:55 bfc43ce2

View on Github →

feat(Logic.Equiv.Basic): dependent version of Equiv.prodUnique (#5817)

Estimated changes

Modified Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.coe_sigmaUnique

added def Equiv.sigmaPUnit

added def Equiv.sigmaUnique

added theorem Equiv.sigmaUnique_apply

added theorem Equiv.sigmaUnique_symm_apply