Theorem RCLike.instPosMulReflectLE

Modification history

2025-02-19 19:52
Mathlib/Analysis/RCLike/Basic.lean
perf: turn `PosMulMono` and friends into classes (#22090) …
Modified RCLike.instPosMulReflectLEView on Github →
2025-02-03 16:47
Mathlib/Analysis/RCLike/Basic.lean
feat(Analysis/RCLike/Basic): PosMulReflectLE (#21351) …
Added RCLike.instPosMulReflectLEView on Github →