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.