Skip to content

Commit 024eb1d

Browse files
mathlib-nightly-testing[bot]mathlib-nightly-testing[bot]
committed
2 parents 94a13bd + 08becba commit 024eb1d

124 files changed

Lines changed: 2121 additions & 1083 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/build_template.yml‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -310,13 +310,19 @@ jobs:
310310
# cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
311311
echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
312312
if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
313-
git checkout "$PREV_SHA"
314-
../tools-branch/.lake/build/bin/cache get
315-
# Run again with --repo, to ensure we actually get the oleans.
316-
../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
317-
318-
echo "Switching back to branch head"
319-
git checkout "$ORIG_SHA"
313+
# Skip warmup if the previous commit uses a different toolchain
314+
PREV_TOOLCHAIN=$(git show "$PREV_SHA:lean-toolchain" 2>/dev/null || true)
315+
if [[ "$PREV_TOOLCHAIN" != "$(cat lean-toolchain)" ]]; then
316+
echo "Previous commit $PREV_SHA uses a different toolchain ($PREV_TOOLCHAIN); skipping warmup."
317+
else
318+
git checkout "$PREV_SHA"
319+
../tools-branch/.lake/build/bin/cache get
320+
# Run again with --repo, to ensure we actually get the oleans.
321+
../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
322+
323+
echo "Switching back to branch head"
324+
git checkout "$ORIG_SHA"
325+
fi
320326
else
321327
echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
322328
fi

‎Mathlib.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
178178
public import Mathlib.Algebra.Category.ModuleCat.Presheaf
179179
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
180180
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
181+
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
181182
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
182183
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
183184
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
@@ -4389,6 +4390,7 @@ public import Mathlib.FieldTheory.RatFunc.AsPolynomial
43894390
public import Mathlib.FieldTheory.RatFunc.Basic
43904391
public import Mathlib.FieldTheory.RatFunc.Defs
43914392
public import Mathlib.FieldTheory.RatFunc.Degree
4393+
public import Mathlib.FieldTheory.RatFunc.IntermediateField
43924394
public import Mathlib.FieldTheory.RatFunc.Luroth
43934395
public import Mathlib.FieldTheory.Relrank
43944396
public import Mathlib.FieldTheory.Separable
@@ -7291,7 +7293,6 @@ public import Mathlib.Topology.Algebra.Module.Alternating.Basic
72917293
public import Mathlib.Topology.Algebra.Module.Alternating.Topology
72927294
public import Mathlib.Topology.Algebra.Module.Basic
72937295
public import Mathlib.Topology.Algebra.Module.Cardinality
7294-
public import Mathlib.Topology.Algebra.Module.CharacterSpace
72957296
public import Mathlib.Topology.Algebra.Module.ClosedSubmodule
72967297
public import Mathlib.Topology.Algebra.Module.Compact
72977298
public import Mathlib.Topology.Algebra.Module.Determinant
@@ -7308,18 +7309,19 @@ public import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
73087309
public import Mathlib.Topology.Algebra.Module.Multilinear.Topology
73097310
public import Mathlib.Topology.Algebra.Module.PerfectPairing
73107311
public import Mathlib.Topology.Algebra.Module.PerfectSpace
7311-
public import Mathlib.Topology.Algebra.Module.PointwiseConvergence
73127312
public import Mathlib.Topology.Algebra.Module.Simple
7313+
public import Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
73137314
public import Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
73147315
public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
7316+
public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
73157317
public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
7318+
public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
7319+
public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual
73167320
public import Mathlib.Topology.Algebra.Module.Star
73177321
public import Mathlib.Topology.Algebra.Module.StrongTopology
73187322
public import Mathlib.Topology.Algebra.Module.TopDualPairing
73197323
public import Mathlib.Topology.Algebra.Module.TransferInstance
73207324
public import Mathlib.Topology.Algebra.Module.UniformConvergence
7321-
public import Mathlib.Topology.Algebra.Module.WeakBilin
7322-
public import Mathlib.Topology.Algebra.Module.WeakDual
73237325
public import Mathlib.Topology.Algebra.Monoid
73247326
public import Mathlib.Topology.Algebra.Monoid.AddChar
73257327
public import Mathlib.Topology.Algebra.Monoid.Defs

‎Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean‎

Lines changed: 244 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
1+
/-
2+
Copyright (c) 2026 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Category.ModuleCat.Presheaf
9+
public import Mathlib.Algebra.Category.Ring.FilteredColimits
10+
public import Mathlib.CategoryTheory.Filtered.FinallySmall
11+
public import Mathlib.CategoryTheory.Monoidal.Limits.Colimits
12+
13+
/-!
14+
# The colimit module of a presheaf of modules on a cofiltered category
15+
16+
Given a colimit cocone `cR` for a presheaf of rings `R` on a cofiltered category `C`,
17+
`M` a presheaf of modules over `R`, and a colimit cocone `cM` for the underlying
18+
functor `Cᵒᵖ ⥤ AddCommGrpCat` of `M`, we define a structure of module over `cR.pt`
19+
on a type-synonym `PresheafOfModules.ModuleColimit` for `cM.pt`. This extends to
20+
a functor `PresheafOfModules.colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt`.
21+
22+
## TODO (@joelriou)
23+
* Define fiber functors on categories of (pre)sheaves of modules
24+
* Refactor `Mathlib/Algebra/Category/ModuleCat/Stalk.lean` so that it uses
25+
this slightly more general construction.
26+
27+
-/
28+
29+
@[expose] public section
30+
31+
universe w v u
32+
33+
open CategoryTheory Limits MonoidalCategory
34+
35+
attribute [local instance] hasColimitsOfShape_of_finallySmall
36+
IsFiltered.isSifted FinallySmall.preservesColimitsOfShape_of_isFiltered
37+
38+
namespace PresheafOfModules
39+
40+
variable {C : Type u} [Category.{v} C] [LocallySmall.{w} C]
41+
[IsCofiltered C] [InitiallySmall.{w} C]
42+
{R : Cᵒᵖ ⥤ RingCat.{w}} {cR : Cocone R} (hcR : IsColimit cR)
43+
44+
section
45+
46+
variable {M : PresheafOfModules.{w} R} {cM : Cocone M.presheaf} (hcM : IsColimit cM)
47+
{M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf} (hcM' : IsColimit cM')
48+
{M'' : PresheafOfModules.{w} R} {cM'' : Cocone M''.presheaf} (hcM'' : IsColimit cM'')
49+
50+
/-- Given a colimit cocone for a presheaf of rings `R` on a cofiltered category `C`,
51+
`M` a presheaf of modules over `R`, and a colimit cocone `cM` for the underlying
52+
functor `Cᵒᵖ ⥤ AddCommGrpCat` of `M`, this is the type `cM.pt` on which we define
53+
a module structure below. -/
54+
@[nolint unusedArguments]
55+
def ModuleColimit (_ : IsColimit cR) (_ : IsColimit cM) : Type w := cM.pt
56+
57+
instance : AddCommGroup (ModuleColimit hcR hcM) :=
58+
inferInstanceAs (AddCommGroup cM.pt)
59+
60+
namespace ModuleColimit
61+
62+
/-- The cocone for `R ⋙ forget _ ⊗ M.presheaf ⋙ forget _` with point
63+
`ModuleColimit hcR hcM` which allows to define the scalar multiplication
64+
by `cR.pt` on `ModuleColimit hcR hcM`. -/
65+
@[simps]
66+
noncomputable def coconeSMul :
67+
Cocone (R ⋙ forget _ ⊗ M.presheaf ⋙ forget _) where
68+
pt := ModuleColimit hcR hcM
69+
ι.app U := fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
70+
ι.naturality V U f := by
71+
ext ⟨r, m⟩
72+
exact (ConcreteCategory.congr_arg (cM.ι.app U)
73+
(M.map_smul f r m).symm).trans (ConcreteCategory.congr_hom (cM.w f) _)
74+
75+
noncomputable instance : SMul cR.pt (ModuleColimit hcR hcM) where
76+
smul :=
77+
(((isColimitOfPreserves (forget _) hcR).tensor
78+
(isColimitOfPreserves (forget _) hcM)).desc (coconeSMul hcR hcM)).curry
79+
80+
variable (cR) in
81+
/-- The "inclusion" maps to the colimit ring. -/
82+
abbrev ιR {U : Cᵒᵖ} : R.obj U →+* cR.pt := (cR.ι.app U).hom
83+
84+
variable {hcR hcM} in
85+
/-- The "inclusion" maps to the colimit module, as an additive map. -/
86+
noncomputable abbrev ιM {U : Cᵒᵖ} : M.obj U →+ ModuleColimit hcR hcM :=
87+
(cM.ι.app U).hom
88+
89+
@[simp]
90+
lemma smul_eq {U : Cᵒᵖ} (r : R.obj U) (m : M.obj U) :
91+
ιR cR r • ιM (hcR := hcR) (hcM := hcM) m = ιM (r • m) :=
92+
congr_fun (((isColimitOfPreserves (forget _) hcR).tensor
93+
(isColimitOfPreserves (forget _) hcM)).fac (coconeSMul hcR hcM) U) ⟨r, m⟩
94+
95+
variable {hcR hcM} in
96+
lemma ιM_jointly_surjective (m : ModuleColimit hcR hcM) :
97+
∃ (U : Cᵒᵖ) (x : M.obj U), ιM x = m :=
98+
Types.jointly_surjective_of_isColimit
99+
(isColimitOfPreserves (forget AddCommGrpCat) hcM) m
100+
101+
set_option backward.isDefEq.respectTransparency false in
102+
variable {hcR hcM hcM'} in
103+
lemma ιM_jointly_surjective₂ (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM') :
104+
∃ (U : Cᵒᵖ) (x : M.obj U) (x' : M'.obj U), ιM x = m ∧ ιM x' = m' := by
105+
obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
106+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
107+
(isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, m'⟩
108+
rw [Prod.ext_iff] at h
109+
obtain ⟨rfl, rfl⟩ := h
110+
exact ⟨U, x, x', rfl, rfl⟩
111+
112+
set_option backward.isDefEq.respectTransparency false in
113+
variable {hcR hcM hcM' hcM''} in
114+
lemma ιM_jointly_surjective₃ (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM')
115+
(m'' : ModuleColimit hcR hcM'') :
116+
∃ (U : Cᵒᵖ) (x : M.obj U) (x' : M'.obj U) (x'' : M''.obj U),
117+
ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m'' := by
118+
obtain ⟨U, ⟨x, x', x''⟩, h⟩ := Types.jointly_surjective_of_isColimit
119+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
120+
((isColimitOfPreserves (forget AddCommGrpCat) hcM').tensor
121+
(isColimitOfPreserves (forget AddCommGrpCat) hcM''))) ⟨m, m', m''⟩
122+
rw [Prod.ext_iff, Prod.ext_iff] at h
123+
obtain ⟨rfl, rfl, rfl⟩ := h
124+
exact ⟨U, x, x', x'', rfl, rfl, rfl⟩
125+
126+
include hcR in
127+
lemma ιR_jointly_surjective (r : cR.pt) :
128+
∃ (U : Cᵒᵖ) (a : R.obj U), ιR cR a = r :=
129+
Types.jointly_surjective_of_isColimit
130+
(isColimitOfPreserves (forget RingCat) hcR) r
131+
132+
set_option backward.isDefEq.respectTransparency false in
133+
variable {hcR hcM} in
134+
lemma jointly_surjective₂ (r : cR.pt) (m : ModuleColimit hcR hcM) :
135+
∃ (U : Cᵒᵖ) (a : R.obj U) (x : M.obj U),
136+
ιR cR a = r ∧ ιM x = m := by
137+
obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
138+
((isColimitOfPreserves (forget RingCat) hcR).tensor
139+
(isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨r, m⟩
140+
rw [Prod.ext_iff] at h
141+
obtain ⟨rfl, rfl⟩ := h
142+
exact ⟨U, a, x, rfl, rfl⟩
143+
144+
set_option backward.isDefEq.respectTransparency false in
145+
variable {hcR hcM} in
146+
lemma jointly_surjective₃ (r₁ r₂ : cR.pt) (m : ModuleColimit hcR hcM) :
147+
∃ (U : Cᵒᵖ) (a₁ a₂ : R.obj U) (x : M.obj U),
148+
ιR cR a₁ = r₁ ∧ ιR cR a₂ = r₂ ∧ ιM x = m := by
149+
obtain ⟨U, ⟨a₁, a₂, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
150+
((isColimitOfPreserves (forget RingCat) hcR).tensor
151+
((isColimitOfPreserves (forget RingCat) hcR).tensor
152+
(isColimitOfPreserves (forget AddCommGrpCat) hcM))) ⟨r₁, r₂, m⟩
153+
rw [Prod.ext_iff, Prod.ext_iff] at h
154+
obtain ⟨rfl, rfl, rfl⟩ := h
155+
exact ⟨U, a₁, a₂, x, rfl, rfl, rfl⟩
156+
157+
set_option backward.isDefEq.respectTransparency false in
158+
variable {hcR hcM hcM'} in
159+
lemma jointly_surjective₃' (r : cR.pt) (m₁ : ModuleColimit hcR hcM) (m₂ : ModuleColimit hcR hcM') :
160+
∃ (U : Cᵒᵖ) (a : R.obj U) (x₁ : M.obj U) (x₂ : M'.obj U),
161+
ιR cR a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂ := by
162+
obtain ⟨U, ⟨a, x₁, x₂⟩, h⟩ := Types.jointly_surjective_of_isColimit
163+
((isColimitOfPreserves (forget RingCat) hcR).tensor
164+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
165+
(isColimitOfPreserves (forget AddCommGrpCat) hcM'))) ⟨r, m₁, m₂⟩
166+
rw [Prod.ext_iff, Prod.ext_iff] at h
167+
obtain ⟨rfl, rfl, rfl⟩ := h
168+
exact ⟨U, a, x₁, x₂, rfl, rfl, rfl⟩
169+
170+
noncomputable instance : Module cR.pt (ModuleColimit hcR hcM) where
171+
mul_smul r₁ r₂ m := by
172+
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
173+
simp only [smul_eq, ← mul_smul, ← map_mul]
174+
one_smul m := by
175+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
176+
simpa using smul_eq hcR hcM 1 m
177+
zero_smul m := by
178+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
179+
simpa using smul_eq hcR hcM 0 m
180+
smul_zero r := by
181+
obtain ⟨U, r, rfl⟩ := ιR_jointly_surjective hcR r
182+
simpa using smul_eq hcR hcM r 0
183+
smul_add r m₁ m₂ := by
184+
obtain ⟨U, r, m₁, m₂, rfl, rfl, rfl⟩ := jointly_surjective₃' r m₁ m₂
185+
simp only [smul_eq, smul_add, ← map_add]
186+
add_smul r₁ r₂ m := by
187+
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
188+
simp only [smul_eq, ← map_add, add_smul]
189+
190+
section
191+
192+
variable {M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf}
193+
(hcM' : IsColimit cM')
194+
195+
/-- The linear map between the colimit modules induced by a morphism of modules. -/
196+
noncomputable def map (f : M ⟶ M') :
197+
ModuleColimit hcR hcM →ₗ[cR.pt] ModuleColimit hcR hcM' where
198+
toFun := hcM.desc ((Cocone.precompose ((toPresheaf _).map f)).obj cM')
199+
map_add' _ _ := map_add _ _ _
200+
map_smul' r m := by
201+
obtain ⟨U, r, m, rfl, rfl⟩ := ModuleColimit.jointly_surjective₂ r m
202+
let c := (Cocone.precompose ((toPresheaf _).map f)).obj cM'
203+
have h₁ := ConcreteCategory.congr_hom (hcM.fac c U) (r • m)
204+
have h₂ := ConcreteCategory.congr_hom (hcM.fac c U) m
205+
dsimp [c] at h₁ h₂ ⊢
206+
rw [ModuleColimit.smul_eq]
207+
erw [h₁, h₂, ModuleColimit.smul_eq, ← (f.app U).hom.map_smul]
208+
rfl
209+
210+
@[simp]
211+
lemma map_apply (f : M ⟶ M') {U : Cᵒᵖ} (m : M.obj U) :
212+
dsimp% map hcR hcM hcM' f (ιM m) = ιM (f.app _ m) :=
213+
ConcreteCategory.congr_hom (hcM.fac ((Cocone.precompose ((toPresheaf _).map f)).obj cM') U) m
214+
215+
@[simp]
216+
lemma map_id : map hcR hcM hcM (𝟙 M) = .id := by
217+
ext m
218+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
219+
simp
220+
221+
lemma comp_map
222+
(f : M ⟶ M')
223+
{M'' : PresheafOfModules.{w} R} {cM'' : Cocone M''.presheaf}
224+
(hcM'' : IsColimit cM'') (g : M' ⟶ M'') :
225+
(map hcR hcM' hcM'' g).comp (map hcR hcM hcM' f) = map hcR hcM hcM'' (f ≫ g) := by
226+
ext m
227+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
228+
simp
229+
230+
end
231+
232+
end ModuleColimit
233+
234+
end
235+
236+
/-- The colimit module functor from the category of presheaves of modules
237+
over a presheaf of rings `R` on a cofiltered category to the category
238+
of modules over a colimit of `R`. -/
239+
noncomputable def colimitFunctor : PresheafOfModules.{w} R ⥤ ModuleCat.{w} cR.pt where
240+
obj M := ModuleCat.of _ (ModuleColimit hcR (colimit.isColimit M.presheaf))
241+
map f := ModuleCat.ofHom (ModuleColimit.map _ _ _ f)
242+
map_comp f g := by ext : 1; exact (ModuleColimit.comp_map ..).symm
243+
244+
end PresheafOfModules

‎Mathlib/Algebra/Group/Subgroup/Defs.lean‎

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -674,20 +674,32 @@ def normalizer (S : Set G) : Subgroup G where
674674

675675
@[deprecated (since := "2026-03-19")] alias setNormalizer := normalizer
676676

677-
variable {H}
677+
variable {H} {S : Set G}
678678

679679
@[to_additive]
680-
theorem mem_normalizer_iff {g : G} : g ∈ normalizer H ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
680+
theorem mem_set_normalizer_iff {g : G} : g ∈ normalizer S ↔ ∀ h, h ∈ S ↔ g * h * g⁻¹ ∈ S :=
681681
Iff.rfl
682682

683683
@[to_additive]
684-
theorem mem_normalizer_iff'' {g : G} : g ∈ normalizer H ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
685-
rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]
684+
theorem mem_set_normalizer_iff'' {g : G} : g ∈ normalizer S ↔ ∀ h : G, h ∈ S ↔ g⁻¹ * h * g ∈ S := by
685+
rw [← inv_mem_iff (x := g), mem_set_normalizer_iff, inv_inv]
686+
687+
@[to_additive]
688+
theorem mem_set_normalizer_iff' {g : G} : g ∈ normalizer S ↔ ∀ n, n * g ∈ S ↔ g * n ∈ S :=
689+
⟨fun h n ↦ by rw [h, mul_assoc, mul_inv_cancel_right],
690+
fun h n ↦ by rw [mul_assoc, ← h, inv_mul_cancel_right]⟩
691+
692+
@[to_additive]
693+
theorem mem_normalizer_iff {g : G} : g ∈ normalizer H ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
694+
mem_set_normalizer_iff
695+
696+
@[to_additive]
697+
theorem mem_normalizer_iff'' {g : G} : g ∈ normalizer H ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H :=
698+
mem_set_normalizer_iff''
686699

687700
@[to_additive]
688701
theorem mem_normalizer_iff' {g : G} : g ∈ normalizer H ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
689-
⟨fun h n ↦ by rw [← SetLike.mem_coe, ← SetLike.mem_coe, h, mul_assoc, mul_inv_cancel_right],
690-
fun h n ↦ by rw [SetLike.mem_coe, SetLike.mem_coe, mul_assoc, ← h, inv_mul_cancel_right]⟩
702+
mem_set_normalizer_iff'
691703

692704
@[to_additive]
693705
theorem le_normalizer : H ≤ normalizer H := fun x xH n => by

0 commit comments

Comments
 (0)