Commit 2023-03-14 15:36 3fc0b254

View on Github →

chore(analysis/inner_product_space): rename _sym to _symm (#18580) This is the preferred spelling of symmetric in mathlib. sym refers to the type of unordered pairs.

Estimated changes

Modified src/analysis/inner_product_space/adjoint.lean

Modified src/analysis/inner_product_space/basic.lean

deleted theorem inner_abs_conj_sym

added theorem inner_abs_conj_symm

deleted theorem inner_conj_sym

added theorem inner_conj_symm

deleted theorem inner_eq_zero_sym

added theorem inner_eq_zero_symm

deleted theorem inner_product_space.of_core.inner_abs_conj_sym

added theorem inner_product_space.of_core.inner_abs_conj_symm

deleted theorem inner_product_space.of_core.inner_conj_sym

added theorem inner_product_space.of_core.inner_conj_symm

modified theorem real_inner_comm

Modified src/analysis/inner_product_space/dual.lean

Modified src/analysis/inner_product_space/gram_schmidt_ortho.lean

Modified src/analysis/inner_product_space/l2_space.lean

Modified src/analysis/inner_product_space/pi_L2.lean

Modified src/analysis/inner_product_space/projection.lean

Modified src/analysis/inner_product_space/symmetric.lean

Modified src/analysis/quaternion.lean

Modified src/linear_algebra/matrix/ldl.lean

Modified src/linear_algebra/matrix/pos_def.lean

Modified src/measure_theory/function/l2_space.lean