Commit 2026-02-10 23:11 87c19abc

View on Github →

feat(Analysis/Normed/Module/{HahnBanach, Dual}): Weaken [NormedAddCommGroup] to seminormed (#34585) This PR weakens the assumption [NormedAddCommGroup] to [SeminormedAddCommGroup] in

  • exists_dual_vector (which now assumes (h : ‖x‖ ≠ 0) instead of (h :x ≠ 0))
  • exists_dual_vector''
  • NormedSpace.norm_le_dual_bound
  • NormedSpace.inclusionInDoubleDualLi

Estimated changes

deleted theorem coord_norm'
modified theorem exists_dual_vector