Theorem UniformSpace.Completion.inner_coe

Modification history

2025-05-03 01:57
Mathlib/Analysis/InnerProductSpace/Completion.lean
chore(Analysis/InnerProductSpace): make `𝕜` an explicit argument of `inner` (#24499) …
Modified UniformSpace.Completion.inner_coeView on Github →
2024-12-20 05:04
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore(Analysis/InnerProductSpace): split large file (#20046) …
Modified UniformSpace.Completion.inner_coeView on Github →
2023-05-25 17:58
Mathlib/Analysis/InnerProductSpace/Basic.lean
feat: port Analysis.InnerProductSpace.Basic (#4280) …
Added UniformSpace.Completion.inner_coeView on Github →