Commit 2025-04-23 04:28 3d26669d

View on Github →

feat: 0 < re ⟪x, x⟫ ↔ x ≠ 0 (#24235) From Toric

Estimated changes

added theorem inner_self_pos
modified theorem real_inner_self_nonpos
added theorem real_inner_self_pos