mathlib
274b5309 - feat(data/equiv/basic): add `add_equiv.to_int_linear_equiv` (#11456)

Commit
3 years ago
feat(data/equiv/basic): add `add_equiv.to_int_linear_equiv` (#11456) as written by @adamtopaz on [zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/injections.20to.20equiv/near/268038978) Co-authored-by: Adam Topaz <github@adamtopaz.com>
Author
Parents
Loading