Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 05bd61d

Browse files
urkudurkud
committed
chore(analysis): move more code out of analysis.normed_space.basic (#10055)
1 parent 8390325 commit 05bd61d

File tree

5 files changed

+201
-154
lines changed

5 files changed

+201
-154
lines changed

‎src/analysis/normed/group/completion.lean‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/-
2+
Copyright (c) 2021 Heather Macbeth. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Heather Macbeth
5+
-/
6+
import analysis.normed.group.basic
7+
import topology.algebra.group_completion
8+
import topology.metric_space.completion
9+
10+
/-!
11+
# Completion of a normed group
12+
13+
In this file we prove that the completion of a (semi)normed group is a normed group.
14+
15+
## Tags
16+
17+
normed group, completion
18+
-/
19+
20+
noncomputable theory
21+
22+
namespace uniform_space
23+
namespace completion
24+
25+
variables (E : Type*)
26+
27+
instance [uniform_space E] [has_norm E] :
28+
has_norm (completion E) :=
29+
{ norm := completion.extension has_norm.norm }
30+
31+
@[simp] lemma norm_coe {E} [semi_normed_group E] (x : E) :
32+
∥(x : completion E)∥ = ∥x∥ :=
33+
completion.extension_coe uniform_continuous_norm x
34+
35+
instance [semi_normed_group E] : normed_group (completion E) :=
36+
{ dist_eq :=
37+
begin
38+
intros x y,
39+
apply completion.induction_on₂ x y; clear x y,
40+
{ refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
41+
exact continuous.comp completion.continuous_extension continuous_sub },
42+
{ intros x y,
43+
rw [← completion.coe_sub, norm_coe, metric.completion.dist_eq, dist_eq_norm] }
44+
end,
45+
.. uniform_space.completion.add_comm_group,
46+
.. metric.completion.metric_space }
47+
48+
end completion
49+
end uniform_space

‎src/analysis/normed/group/hom_completion.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Patrick Massot
55
-/
66

77
import analysis.normed.group.hom
8+
import analysis.normed.group.completion
89
/-!
910
# Completion of normed group homs
1011

‎src/analysis/normed/group/infinite_sum.lean‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
/-
2+
Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sébastien Gouëzel, Heather Macbeth, Johannes Hölzl, Yury Kudryashov
5+
-/
6+
import analysis.normed.group.basic
7+
import topology.instances.nnreal
8+
9+
/-!
10+
# Infinite sums in (semi)normed groups
11+
12+
In a complete (semi)normed group,
13+
14+
- `summable_iff_vanishing_norm`: a series `∑' i, f i` is summable if and only if for any `ε > 0`,
15+
there exists a finite set `s` such that the sum `∑ i in t, f i` over any finite set `t` disjoint
16+
with `s` has norm less than `ε`;
17+
18+
- `summable_of_norm_bounded`, `summable_of_norm_bounded_eventually`: if `∥f i∥` is bounded above by
19+
a summable series `∑' i, g i`, then `∑' i, f i` is summable as well; the same is true if the
20+
inequality hold only off some finite set.
21+
22+
- `tsum_of_norm_bounded`, `has_sum.norm_le_of_bounded`: if `∥f i∥ ≤ g i`, where `∑' i, g i` is a
23+
summable series, then `∥∑' i, f i∥ ≤ ∑' i, g i`.
24+
25+
## Tags
26+
27+
infinite series, absolute convergence, normed group
28+
-/
29+
30+
open_locale classical big_operators topological_space nnreal
31+
open finset filter metric
32+
33+
variables {ι α E F : Type*} [semi_normed_group E] [semi_normed_group F]
34+
35+
lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → E} :
36+
cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔
37+
∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
38+
begin
39+
rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff],
40+
{ simp only [ball_zero_eq, set.mem_set_of_eq] },
41+
{ rintros s t hst ⟨s', hs'⟩,
42+
exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ }
43+
end
44+
45+
lemma summable_iff_vanishing_norm [complete_space E] {f : ι → E} :
46+
summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
47+
by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]
48+
49+
lemma cauchy_seq_finset_of_norm_bounded {f : ι → E} (g : ι → ℝ) (hg : summable g)
50+
(h : ∀i, ∥f i∥ ≤ g i) : cauchy_seq (λ s : finset ι, ∑ i in s, f i) :=
51+
cauchy_seq_finset_iff_vanishing_norm.2 $ assume ε hε,
52+
let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hg ε hε in
53+
⟨s, assume t ht,
54+
have ∥∑ i in t, g i∥ < ε := hs t ht,
55+
have nn : 0 ≤ ∑ i in t, g i := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
56+
lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
57+
by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
58+
59+
lemma cauchy_seq_finset_of_summable_norm {f : ι → E} (hf : summable (λa, ∥f a∥)) :
60+
cauchy_seq (λ s : finset ι, ∑ a in s, f a) :=
61+
cauchy_seq_finset_of_norm_bounded _ hf (assume i, le_refl _)
62+
63+
/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
64+
its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
65+
with sum `a`. -/
66+
lemma has_sum_of_subseq_of_summable {f : ι → E} (hf : summable (λa, ∥f a∥))
67+
{s : α → finset ι} {p : filter α} [ne_bot p]
68+
(hs : tendsto s p at_top) {a : E} (ha : tendsto (λ b, ∑ i in s b, f i) p (𝓝 a)) :
69+
has_sum f a :=
70+
tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hs ha
71+
72+
lemma has_sum_iff_tendsto_nat_of_summable_norm {f : ℕ → E} {a : E} (hf : summable (λi, ∥f i∥)) :
73+
has_sum f a ↔ tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) :=
74+
⟨λ h, h.tendsto_sum_nat,
75+
λ h, has_sum_of_subseq_of_summable hf tendsto_finset_range h⟩
76+
77+
/-- The direct comparison test for series: if the norm of `f` is bounded by a real function `g`
78+
which is summable, then `f` is summable. -/
79+
lemma summable_of_norm_bounded
80+
[complete_space E] {f : ι → E} (g : ι → ℝ) (hg : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
81+
summable f :=
82+
by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
83+
84+
lemma has_sum.norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ}
85+
(hf : has_sum f a) (hg : has_sum g b) (h : ∀ i, ∥f i∥ ≤ g i) :
86+
∥a∥ ≤ b :=
87+
le_of_tendsto_of_tendsto' hf.norm hg $ λ s, norm_sum_le_of_le _ $ λ i hi, h i
88+
89+
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
90+
summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥∑' i, f i∥ ≤ ∑' i, g i`. Note that we do not
91+
assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
92+
lemma tsum_of_norm_bounded {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a)
93+
(h : ∀ i, ∥f i∥ ≤ g i) :
94+
∥∑' i : ι, f i∥ ≤ a :=
95+
begin
96+
by_cases hf : summable f,
97+
{ exact hf.has_sum.norm_le_of_bounded hg h },
98+
{ rw [tsum_eq_zero_of_not_summable hf, norm_zero],
99+
exact ge_of_tendsto' hg (λ s, sum_nonneg $ λ i hi, (norm_nonneg _).trans (h i)) }
100+
end
101+
102+
/-- If `∑' i, ∥f i∥` is summable, then `∥∑' i, f i∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume
103+
that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
104+
lemma norm_tsum_le_tsum_norm {f : ι → E} (hf : summable (λi, ∥f i∥)) :
105+
∥∑' i, f i∥ ≤ ∑' i, ∥f i∥ :=
106+
tsum_of_norm_bounded hf.has_sum $ λ i, le_rfl
107+
108+
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
109+
summable, and for all `i`, `∥f i∥₊ ≤ g i`, then `∥∑' i, f i∥₊ ≤ ∑' i, g i`. Note that we
110+
do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
111+
space. -/
112+
lemma tsum_of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : has_sum g a)
113+
(h : ∀ i, ∥f i∥₊ ≤ g i) :
114+
∥∑' i : ι, f i∥₊ ≤ a :=
115+
begin
116+
simp only [← nnreal.coe_le_coe, ← nnreal.has_sum_coe, coe_nnnorm] at *,
117+
exact tsum_of_norm_bounded hg h
118+
end
119+
120+
/-- If `∑' i, ∥f i∥₊` is summable, then `∥∑' i, f i∥₊ ≤ ∑' i, ∥f i∥₊`. Note that
121+
we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
122+
space. -/
123+
lemma nnnorm_tsum_le {f : ι → E} (hf : summable (λi, ∥f i∥₊)) :
124+
∥∑' i, f i∥₊ ≤ ∑' i, ∥f i∥₊ :=
125+
tsum_of_nnnorm_bounded hf.has_sum (λ i, le_rfl)
126+
127+
variable [complete_space E]
128+
129+
/-- Variant of the direct comparison test for series: if the norm of `f` is eventually bounded by a
130+
real function `g` which is summable, then `f` is summable. -/
131+
lemma summable_of_norm_bounded_eventually {f : ι → E} (g : ι → ℝ) (hg : summable g)
132+
(h : ∀ᶠ i in cofinite, ∥f i∥ ≤ g i) : summable f :=
133+
begin
134+
replace h := mem_cofinite.1 h,
135+
refine h.summable_compl_iff.mp _,
136+
refine summable_of_norm_bounded _ (h.summable_compl_iff.mpr hg) _,
137+
rintros ⟨a, h'⟩,
138+
simpa using h'
139+
end
140+
141+
lemma summable_of_nnnorm_bounded {f : ι → E} (g : ι → ℝ≥0) (hg : summable g)
142+
(h : ∀i, ∥f i∥₊ ≤ g i) : summable f :=
143+
summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
144+
145+
lemma summable_of_summable_norm {f : ι → E} (hf : summable (λa, ∥f a∥)) : summable f :=
146+
summable_of_norm_bounded _ hf (assume i, le_refl _)
147+
148+
lemma summable_of_summable_nnnorm {f : ι → E} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
149+
summable_of_nnnorm_bounded _ hf (assume i, le_refl _)

‎src/analysis/normed_space/basic.lean‎

Lines changed: 1 addition & 153 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import topology.algebra.group_completion
1010
import topology.instances.ennreal
1111
import topology.metric_space.completion
1212
import topology.sequences
13-
import analysis.normed.group.basic
13+
import analysis.normed.group.infinite_sum
1414

1515
/-!
1616
# Normed spaces
@@ -949,129 +949,6 @@ instance : normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E) :=
949949

950950
end restrict_scalars
951951

952-
section summable
953-
open_locale classical
954-
open finset filter
955-
variables [semi_normed_group α] [semi_normed_group β]
956-
957-
lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → α} :
958-
cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔
959-
∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
960-
begin
961-
rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff],
962-
{ simp only [ball_zero_eq, set.mem_set_of_eq] },
963-
{ rintros s t hst ⟨s', hs'⟩,
964-
exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ }
965-
end
966-
967-
lemma summable_iff_vanishing_norm [complete_space α] {f : ι → α} :
968-
summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
969-
by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]
970-
971-
lemma cauchy_seq_finset_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hg : summable g)
972-
(h : ∀i, ∥f i∥ ≤ g i) : cauchy_seq (λ s : finset ι, ∑ i in s, f i) :=
973-
cauchy_seq_finset_iff_vanishing_norm.2 $ assume ε hε,
974-
let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hg ε hε in
975-
⟨s, assume t ht,
976-
have ∥∑ i in t, g i∥ < ε := hs t ht,
977-
have nn : 0 ≤ ∑ i in t, g i := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
978-
lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
979-
by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
980-
981-
lemma cauchy_seq_finset_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) :
982-
cauchy_seq (λ s : finset ι, ∑ a in s, f a) :=
983-
cauchy_seq_finset_of_norm_bounded _ hf (assume i, le_refl _)
984-
985-
/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
986-
its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
987-
with sum `a`. -/
988-
lemma has_sum_of_subseq_of_summable {f : ι → α} (hf : summable (λa, ∥f a∥))
989-
{s : γ → finset ι} {p : filter γ} [ne_bot p]
990-
(hs : tendsto s p at_top) {a : α} (ha : tendsto (λ b, ∑ i in s b, f i) p (𝓝 a)) :
991-
has_sum f a :=
992-
tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hs ha
993-
994-
lemma has_sum_iff_tendsto_nat_of_summable_norm {f : ℕ → α} {a : α} (hf : summable (λi, ∥f i∥)) :
995-
has_sum f a ↔ tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) :=
996-
⟨λ h, h.tendsto_sum_nat,
997-
λ h, has_sum_of_subseq_of_summable hf tendsto_finset_range h⟩
998-
999-
/-- The direct comparison test for series: if the norm of `f` is bounded by a real function `g`
1000-
which is summable, then `f` is summable. -/
1001-
lemma summable_of_norm_bounded
1002-
[complete_space α] {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
1003-
summable f :=
1004-
by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
1005-
1006-
lemma has_sum.norm_le_of_bounded {f : ι → α} {g : ι → ℝ} {a : α} {b : ℝ}
1007-
(hf : has_sum f a) (hg : has_sum g b) (h : ∀ i, ∥f i∥ ≤ g i) :
1008-
∥a∥ ≤ b :=
1009-
le_of_tendsto_of_tendsto' hf.norm hg $ λ s, norm_sum_le_of_le _ $ λ i hi, h i
1010-
1011-
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
1012-
summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥∑' i, f i∥ ≤ ∑' i, g i`. Note that we do not
1013-
assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
1014-
lemma tsum_of_norm_bounded {f : ι → α} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a)
1015-
(h : ∀ i, ∥f i∥ ≤ g i) :
1016-
∥∑' i : ι, f i∥ ≤ a :=
1017-
begin
1018-
by_cases hf : summable f,
1019-
{ exact hf.has_sum.norm_le_of_bounded hg h },
1020-
{ rw [tsum_eq_zero_of_not_summable hf, norm_zero],
1021-
exact ge_of_tendsto' hg (λ s, sum_nonneg $ λ i hi, (norm_nonneg _).trans (h i)) }
1022-
end
1023-
1024-
/-- If `∑' i, ∥f i∥` is summable, then `∥∑' i, f i∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume
1025-
that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
1026-
lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) :
1027-
∥∑' i, f i∥ ≤ ∑' i, ∥f i∥ :=
1028-
tsum_of_norm_bounded hf.has_sum $ λ i, le_rfl
1029-
1030-
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
1031-
summable, and for all `i`, `nnnorm (f i) ≤ g i`, then `nnnorm (∑' i, f i) ≤ ∑' i, g i`. Note that we
1032-
do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
1033-
space. -/
1034-
lemma tsum_of_nnnorm_bounded {f : ι → α} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : has_sum g a)
1035-
(h : ∀ i, nnnorm (f i) ≤ g i) :
1036-
nnnorm (∑' i : ι, f i) ≤ a :=
1037-
begin
1038-
simp only [← nnreal.coe_le_coe, ← nnreal.has_sum_coe, coe_nnnorm] at *,
1039-
exact tsum_of_norm_bounded hg h
1040-
end
1041-
1042-
/-- If `∑' i, nnnorm (f i)` is summable, then `nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i)`. Note that
1043-
we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
1044-
space. -/
1045-
lemma nnnorm_tsum_le {f : ι → α} (hf : summable (λi, nnnorm (f i))) :
1046-
nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i) :=
1047-
tsum_of_nnnorm_bounded hf.has_sum (λ i, le_rfl)
1048-
1049-
variable [complete_space α]
1050-
1051-
/-- Variant of the direct comparison test for series: if the norm of `f` is eventually bounded by a
1052-
real function `g` which is summable, then `f` is summable. -/
1053-
lemma summable_of_norm_bounded_eventually {f : ι → α} (g : ι → ℝ) (hg : summable g)
1054-
(h : ∀ᶠ i in cofinite, ∥f i∥ ≤ g i) : summable f :=
1055-
begin
1056-
replace h := mem_cofinite.1 h,
1057-
refine h.summable_compl_iff.mp _,
1058-
refine summable_of_norm_bounded _ (h.summable_compl_iff.mpr hg) _,
1059-
rintros ⟨a, h'⟩,
1060-
simpa using h'
1061-
end
1062-
1063-
lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
1064-
(h : ∀i, ∥f i∥₊ ≤ g i) : summable f :=
1065-
summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
1066-
1067-
lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
1068-
summable_of_norm_bounded _ hf (assume i, le_refl _)
1069-
1070-
lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
1071-
summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
1072-
1073-
end summable
1074-
1075952
section cauchy_product
1076953

1077954
/-! ## Multiplying two infinite sums in a normed ring
@@ -1192,32 +1069,3 @@ end
11921069
end nat
11931070

11941071
end cauchy_product
1195-
1196-
namespace uniform_space
1197-
namespace completion
1198-
1199-
variables (V : Type*)
1200-
1201-
instance [uniform_space V] [has_norm V] :
1202-
has_norm (completion V) :=
1203-
{ norm := completion.extension has_norm.norm }
1204-
1205-
@[simp] lemma norm_coe {V} [semi_normed_group V] (v : V) :
1206-
∥(v : completion V)∥ = ∥v∥ :=
1207-
completion.extension_coe uniform_continuous_norm v
1208-
1209-
instance [semi_normed_group V] : normed_group (completion V) :=
1210-
{ dist_eq :=
1211-
begin
1212-
intros x y,
1213-
apply completion.induction_on₂ x y; clear x y,
1214-
{ refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
1215-
exact continuous.comp completion.continuous_extension continuous_sub },
1216-
{ intros x y,
1217-
rw [← completion.coe_sub, norm_coe, metric.completion.dist_eq, dist_eq_norm] }
1218-
end,
1219-
.. (show add_comm_group (completion V), by apply_instance),
1220-
.. (show metric_space (completion V), by apply_instance) }
1221-
1222-
end completion
1223-
end uniform_space

‎src/topology/uniform_space/completion.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -452,7 +452,7 @@ cpkg.extend f
452452

453453
variables [separated_space β]
454454

455-
@[simp]lemma extension_coe (hf : uniform_continuous f) (a : α) :
455+
@[simp] lemma extension_coe (hf : uniform_continuous f) (a : α) :
456456
(completion.extension f) a = f a :=
457457
cpkg.extend_coe hf a
458458

0 commit comments

Comments
 (0)