Commit 2025-12-08 17:39 151fb3b2

View on Github →

feat: generalize continuousAt_zero_of_locally_bounded to nontrivially normed fields (#32475) Also:

  • golf the proof a bit
  • in this file, change all [UniformSpace E] [IsUniformAddGroup E] to [TopologicalSpace E] [IsTopologicalAddGroup E] (the statements do not mention the uniform structure)
  • semilinearize LinearMap.clmOfExistsBoundedImage The only downside is an extra [RingHomIsometric σ] assumption, but I think this does not matter (in fact it would be enough to assume continuity of σ, which is always true in practice).

Estimated changes