feat: norm_num extension for Real.sqrt and NNReal.sqrt#21102
Open
dupuisf wants to merge 9 commits intomasterfrom dupuisf/normnum_real_sqrt
+128
Commits
Commits on Jan 26, 2025
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Jan 27, 2025
- committed
- committed
