Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 02:45 b4f87d99

View on Github →

feat(analysis/normed_space): add normed_space 𝕜 (uniform_space.completion E) (#12148)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem lipschitz_with_smul

Created src/analysis/normed_space/completion.lean

added theorem uniform_space.completion.coe_to_complL

added theorem uniform_space.completion.coe_to_complₗᵢ

added theorem uniform_space.completion.norm_to_complL

added def uniform_space.completion.to_complL

added def uniform_space.completion.to_complₗᵢ

Created src/topology/algebra/uniform_mul_action.lean

added theorem uniform_continuous.const_smul

added theorem uniform_space.completion.coe_smul

Modified src/topology/uniform_space/completion.lean

added theorem uniform_space.completion.ext'