Commit 2023-05-23 16:54 ba5ff5ad

View on Github →

refactor(analysis/normed_space/basic): generalize some results to actions by normed_rings (#19053) This only moves the very basic lemmas for now. This should be very easy to forward-port:

  • Let someone port the new file via the normal mechanism
  • Have them delete the duplicate lemmas that appear in CI A few downstream proofs need some small help with unification, as while the old normed_space argument was found by unification, the new has_bounded_smul has to be found by typeclass search.

Estimated changes

added theorem dist_smul_le
added theorem dist_smul₀
added theorem lipschitz_with_smul
added theorem nndist_smul_le
added theorem nndist_smul₀
added theorem nnnorm_smul
added theorem nnnorm_smul_le
added theorem norm_smul
added theorem norm_smul_le
deleted theorem dist_smul_le
deleted theorem dist_smul₀
deleted theorem lipschitz_with_smul
deleted theorem nndist_smul_le
deleted theorem nndist_smul₀
deleted theorem nnnorm_smul
deleted theorem nnnorm_smul_le
deleted theorem norm_smul
deleted theorem norm_smul_le