Commit 2025-11-15 21:39 aff69c90

View on Github →

chore(Analysis/InnerProductSpace/{Dual, LinearMap}): some renames (#31625) Current naming is confusing, innerSL_apply means innerSL x y but innerSL_apply_coe means ⇑(innerSL x)...? So this PR renames these (and others). Renames: Analysis/InnerProductSpace/LinearMap:

  • innerₛₗ_apply_coe -> coe_innerₛₗ_apply
  • innerₛₗ_apply -> innerₛₗ_apply_apply
  • innerₗ_apply -> innerₗ_apply_apply
  • innerSL_apply_coe -> coe_innerSL_apply
  • innerSL_apply -> innerSL_apply_apply
  • innerSLFlip_apply -> innerSLFlip_apply_apply
  • innerSL_real_flip -> flip_innerSL_real Analysis/InnerProductSpace/Dual:
  • InnerProductSpace.toDualMap_apply -> InnerProductSpace.toDualMap_apply_apply
  • InnerProductSpace.toDual_apply -> InnerProductSpace.toDual_apply_apply

Estimated changes

added theorem coe_innerSL_apply
added theorem coe_innerₛₗ_apply
added theorem flip_innerSL_real
deleted theorem innerSLFlip_apply
deleted theorem innerSL_apply
added theorem innerSL_apply_apply
deleted theorem innerSL_apply_coe
deleted theorem innerSL_real_flip
deleted theorem innerₗ_apply
added theorem innerₗ_apply_apply
deleted theorem innerₛₗ_apply
deleted theorem innerₛₗ_apply_coe