Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix(fintype/basic): typo in docstring (#7041)
Browse files Browse the repository at this point in the history
  • Loading branch information
ericrbg committed Apr 5, 2021
1 parent d36d766 commit 5be4463
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/data/fintype/basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1258,7 +1258,7 @@ variables [fintype α]
variables [decidable_eq β]
variables {f : α → β}

/-- `
/--
`bij_inv f` is the unique inverse to a bijection `f`. This acts
as a computable alternative to `function.inv_fun`. -/
def bij_inv (f_bij : bijective f) (b : β) : α :=
Expand Down

0 comments on commit 5be4463

Please sign in to comment.