Commit 2025-11-19 20:40 61876368

View on Github →

perf(Data.Real.Sqrt): make Real.sqrt irreducible (#25856) We try to see what happens if we make Real.sqrt irreducible. There are cases where this makes unification very significantly faster, compare #mathlib4 > Coercion triggers timeout @ 💬. (Migrated manually from #24752)

Estimated changes

modified theorem Real.continuous_sqrt
modified theorem Real.sqrt_nonneg