Commit 2023-07-21 08:49 aa43be2f

View on Github →

feat: add some missing simp lemmas (#6028)

Estimated changes

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem Homeomorph.smulOfNeZero_symm_apply

Modified Mathlib/Topology/Homeomorph.lean

added theorem Homeomorph.symm_trans_apply

Modified Mathlib/Topology/LocalHomeomorph.lean