mathlib
9cdffe9c - refactor(data/fin): shorter proof of `mk.inj_iff` (#5811)

Commit

4 years ago

refactor(data/fin): shorter proof of `mk.inj_iff` (#5811) Co-authors: `lean-gptf`, Yuhuai Wu

Author

Jesse Michael Han

Parents