Commit 2025-07-30 17:41 8be247aa

chore(Analysis): make argument explicit to CFC.sqrt_nonneg and CFC.sqrt_eq_rpow (#27684) These two lemmas had all arguments implicit, which means we have to add implicit argument hints in a few places: sqrt_nonneg (a := a) : 0 ≤ sqrt a. For Real.sqrt_nonneg and similar, the a argument is explicit. Making it explicit here avoids a few type ascriptions and implicit argument hints.