Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-25 21:12 7ee73e4a

View on Github →

feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816) When f : α → β, g : β → α are inverses one way and card α ≤ card β, then they form an equivalence.

Estimated changes