Def LocalEquiv.piecewise

Modification history

2023-12-13 09:43

Mathlib/Logic/Equiv/PartialEquiv.lean

chore: rename LocalEquiv to PartialEquiv (#8984) …

Deleted LocalEquiv.piecewise View on Github →

2023-01-06 13:58

Mathlib/Logic/Equiv/LocalEquiv.lean

feat port: Logic.Equiv.LocalEquiv (#1052) …

Added LocalEquiv.piecewise View on Github →