Commit 2024-04-06 14:26 1c861a03

View on Github →

feat: generalize sq_pos_iff, sq_pos_of_ne_zero (#11743) This was previously about LinearOrderedRing, which is strictly stronger. The new assumptions match sq_nonneg.

Estimated changes

modified theorem sq_pos_iff
modified theorem sq_pos_of_ne_zero