Commit 2025-04-23 20:46 55b90745

View on Github →

chore(InnerProductSpace): follow the naming convention (#24250) A lot of mentions to re were ommitted, but not all, which makes it extra confusing.

Estimated changes

deleted theorem inner_self_nonpos
deleted theorem inner_self_pos
deleted theorem norm_eq_sqrt_inner
added theorem norm_eq_sqrt_re_inner
added theorem re_inner_self_nonpos
added theorem re_inner_self_pos
modified theorem real_inner_self_nonpos
modified theorem real_inner_self_pos