Commit 2025-09-16 10:17 78a7a890

View on Github →

chore: basic grind annotations for Real.sqrt (#29456)

Estimated changes

added theorem Real.sq_sqrt'
modified theorem lt_trichotomy