mathlib
481f9910 - refactor(algebra/{hom/equiv, ring/equiv}): rename `equiv_of_unique_of_unique` to `equiv_of_unique` (#14861)

Commit
3 years ago
refactor(algebra/{hom/equiv, ring/equiv}): rename `equiv_of_unique_of_unique` to `equiv_of_unique` (#14861) This matches [`equiv.equiv_of_unique`](https://leanprover-community.github.io/mathlib_docs/logic/equiv/basic.html#equiv.equiv_of_unique).
Author
Parents
Loading