Theorem Real.sq_sqrt'

Modification history

2025-09-16 10:17
Mathlib/Data/Real/Sqrt.lean
chore: basic grind annotations for Real.sqrt (#29456)
Added Real.sq_sqrt'View on Github →