Def LowerAdjoint.Simps.apply

Modification history

2023-03-08 15:13

Mathlib/Order/Closure.lean

feat: initialize_simps_projections automatically finds coercions (#2045) …

Deleted LowerAdjoint.Simps.apply View on Github →

2023-01-01 23:31

Mathlib/Order/Closure.lean

feat: port Order.Closure (#1263) …

Added LowerAdjoint.Simps.apply View on Github →