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.
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.