Theorem Real.sqrt_eq_iff_eq_mul_self

Modification history

2025-03-04 03:24

Mathlib/Data/Real/Sqrt.lean

chore: remove >6 month old deprecations (#22473)

Deleted Real.sqrt_eq_iff_eq_mul_self View on Github →

2024-08-25 10:33

Mathlib/Data/Real/Sqrt.lean

refactor: Make it so that `sqrt` lemmas don't turn equalities around (#16134) …

Added Real.sqrt_eq_iff_eq_mul_self View on Github →