Commit 2023-03-10 02:21 703e6b75

View on Github →

refactor: use positivity in proofs (#2758)

Possible after #2726

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem zero_lt_one_add_norm_sq'