Theorem Real.mk_le

Modification history

2024-03-08 22:04

Mathlib/Data/Real/Basic.lean

chore: squeeze some non-terminal simps (#11247) …

Modified Real.mk_le View on Github →

2023-01-17 09:04

Mathlib/Data/Real/Basic.lean

feat: port Data.Real.Basic (#1514)

Added Real.mk_le View on Github →