Theorem Measurable.sqrt

Modification history

2024-04-13 10:35

Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

feat: add notation for Real.sqrt (#12056) …

Modified Measurable.sqrt View on Github →

2023-05-21 21:51

Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

feat: port MeasureTheory.Function.SpecialFunctions.Basic (#4175)

Added Measurable.sqrt View on Github →