Commit 2025-03-01 19:37 943d1380

feat: norm_num extension for Real.sqrt and NNReal.sqrt (#21102) This PR introduces a norm_num extension for both Real.sqrt and NNReal.sqrt. While the version for Real.sqrt can handle both integers and rationals, the version for NNReal.sqrt can only deal with integers, due to a limitation of norm_num (i.e. the IsRat type requires a Ring instance). I put the extension directly in Data/Real/Sqrt, but I could put them in a separate file in Tactic/NormNum if this is deemed better. (The obvious downside is that potential users would need to import the file explicitly.)