Def Real.sqrtAux

Modification history

2024-04-06 16:24

Mathlib/Data/Real/Sqrt.lean

chore(Data/Real/Sqrt): delete commented-out incomplete code (#11909) …

Deleted Real.sqrtAux View on Github →

2023-03-08 06:27

Mathlib/Data/Real/Sqrt.lean

feat: port Data.Real.Sqrt (#2674)

Added Real.sqrtAux View on Github →