Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 22:52 f9da68cc

View on Github →

feat(*): a few more fun_uniques (#9938)

Estimated changes

Modified src/data/equiv/basic.lean

modified def equiv.fun_unique

Modified src/linear_algebra/pi.lean

added def linear_equiv.fun_unique

Modified src/topology/algebra/module.lean

added theorem continuous_linear_equiv.coe_fun_unique

added theorem continuous_linear_equiv.coe_fun_unique_symm

added def continuous_linear_equiv.fun_unique

Modified src/topology/homeomorph.lean

added def homeomorph.fun_unique