Commit 2024-08-25 10:33 fb857aaa

View on Github →

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

Estimated changes

Modified Archive/Imo/Imo1959Q2.lean

Modified Archive/Imo/Imo1960Q2.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/Data/Real/Sqrt.lean

added theorem Real.sqrt_eq_iff_eq_mul_self

added theorem Real.sqrt_eq_iff_eq_sq

modified theorem Real.sqrt_eq_iff_mul_self_eq