Theorem UniformSpace.Completion.nnnorm_coe

Modification history

2024-06-29 17:35
Mathlib/Analysis/Normed/Group/Completion.lean
feat: remove completeness assumption in Sobolev inequality (#14262)
Added UniformSpace.Completion.nnnorm_coeView on Github →