diff --git a/Archive.lean b/Archive.lean index 990ddbc04a894f..88bba470b09016 100644 --- a/Archive.lean +++ b/Archive.lean @@ -66,6 +66,7 @@ import Archive.MinimalSheffer import Archive.MiuLanguage.Basic import Archive.MiuLanguage.DecisionNec import Archive.MiuLanguage.DecisionSuf +import Archive.NamedGraphs import Archive.OxfordInvariants.Summer2021.Week3P1 import Archive.Sensitivity import Archive.Wiedijk100Theorems.AbelRuffini diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean new file mode 100644 index 00000000000000..eda6a741f3eb6e --- /dev/null +++ b/Archive/NamedGraphs.lean @@ -0,0 +1,341 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +import Mathlib.Combinatorics.SimpleGraph.QuotientGraph +import Mathlib.Combinatorics.SimpleGraph.Action +import Mathlib.Combinatorics.SimpleGraph.Representation + +/-! +# Named graphs and antipodal quotients + +The dodecahedron has an antipodal involution (distance 5) whose quotient is the +Petersen graph. The 3-cube has an antipodal involution (bitwise complement, distance 3) +whose quotient is K₄. + +## Main definitions + +* `dodecahedronGraph` — the dodecahedron on `Fin 20`, 3-regular, 30 edges +* `petersenGraph` — the Petersen graph on `Fin 10`, as `dodecahedronGraph.quotientGraph` +* `cubeGraph` — the 3-cube Q₃ on `Fin 8`, 3-regular, 12 edges + +## Main results + +* `dodecahedronGraph_regular` — the dodecahedron is 3-regular +* `petersenGraph_regular` — the Petersen graph is 3-regular +* `cubeQuotient_eq_top` — the antipodal quotient of the cube is K₄ + +## Visualizations + +* [Dodecahedron → Petersen quotient](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/dodecahedron-quotient-petersen.jpeg) — the Z₂ antipodal quotient, with fibers color-coded +* [3-Cube → K₄ quotient](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/cube-quotient-k4.jpeg) — the Z₂ antipodal quotient (bitwise complement) + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798 +-/ + +set_option linter.style.nativeDecide false + +open SimpleGraph + +/-! ### The dodecahedron graph -/ + +private def dodecAdjBool (u v : Fin 20) : Bool := + let edges : List (Fin 20 × Fin 20) := [ + (0, 1), (0, 4), (0, 5), (1, 2), (1, 7), (2, 3), (2, 9), (3, 4), (3, 11), (4, 13), + (5, 6), (5, 14), (6, 7), (6, 15), (7, 8), (8, 9), (8, 16), (9, 10), (10, 11), (10, 17), + (11, 12), (12, 13), (12, 18), (13, 14), (14, 19), (15, 16), (15, 19), (16, 17), (17, 18), + (18, 19)] + edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **dodecahedron graph**, the 1-skeleton of the regular dodecahedron. -/ +def dodecahedronGraph : SimpleGraph (Fin 20) where + Adj u v := dodecAdjBool u v + symm u v := by simp only [dodecAdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [dodecAdjBool]; revert u; native_decide⟩ + +instance : DecidableRel dodecahedronGraph.Adj := + fun u v => inferInstanceAs (Decidable (dodecAdjBool u v)) + +/-! ### The antipodal quotient map -/ + +private def dodecAntipodalData : List (Fin 10) := + [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 5, 6, 7, 8, 9, 3, 4, 0, 1, 2] + +private theorem dodecAntipodalData_length : dodecAntipodalData.length = 20 := by native_decide + +/-- The antipodal quotient map: `Fin 20 → Fin 10`. -/ +def dodecAntipodalMap (v : Fin 20) : Fin 10 := + dodecAntipodalData.get (v.cast dodecAntipodalData_length.symm) + +/-! ### The Petersen graph -/ + +/-- The **Petersen graph**, the antipodal quotient of the dodecahedron. -/ +def petersenGraph : SimpleGraph (Fin 10) := + dodecahedronGraph.quotientGraph dodecAntipodalMap + +instance : DecidableRel petersenGraph.Adj := by + intro i j; unfold petersenGraph quotientGraph; simp only; exact instDecidableAnd + +/-- The dodecahedron is 3-regular. -/ +theorem dodecahedronGraph_regular : + ∀ v : Fin 20, (Finset.univ.filter fun w => dodecahedronGraph.Adj v w).card = 3 := by + native_decide + +/-- The dodecahedron has 30 edges. -/ +theorem dodecahedronGraph_edgeCount : + (Finset.univ.filter fun p : Fin 20 × Fin 20 => + p.1 < p.2 ∧ dodecahedronGraph.Adj p.1 p.2).card = 30 := by + native_decide + +/-- The Petersen graph is 3-regular. -/ +theorem petersenGraph_regular : + ∀ v : Fin 10, (Finset.univ.filter fun w => petersenGraph.Adj v w).card = 3 := by + native_decide + +/-- The Petersen graph has 15 edges. -/ +theorem petersenGraph_edgeCount : + (Finset.univ.filter fun p : Fin 10 × Fin 10 => + p.1 < p.2 ∧ petersenGraph.Adj p.1 p.2).card = 15 := by + native_decide + +/-! ### The 3-cube graph -/ + +private def cubeAdjBool (u v : Fin 8) : Bool := + let edges : List (Fin 8 × Fin 8) := [ + (0, 1), (0, 2), (0, 4), (1, 3), (1, 5), (2, 3), (2, 6), (3, 7), + (4, 5), (4, 6), (5, 7), (6, 7)] + edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **3-cube graph** Q₃, the 1-skeleton of the 3-dimensional hypercube. -/ +def cubeGraph : SimpleGraph (Fin 8) where + Adj u v := cubeAdjBool u v + symm u v := by simp only [cubeAdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [cubeAdjBool]; revert u; native_decide⟩ + +instance : DecidableRel cubeGraph.Adj := + fun u v => inferInstanceAs (Decidable (cubeAdjBool u v)) + +/-! ### The cube antipodal quotient -/ + +private def cubeAntipodalData : List (Fin 4) := [0, 1, 2, 3, 3, 2, 1, 0] + +private theorem cubeAntipodalData_length : cubeAntipodalData.length = 8 := by native_decide + +/-- The antipodal quotient map on Q₃: `Fin 8 → Fin 4`. -/ +def cubeAntipodalMap (v : Fin 8) : Fin 4 := + cubeAntipodalData.get (v.cast cubeAntipodalData_length.symm) + +/-- The antipodal quotient of the 3-cube. -/ +def cubeQuotientGraph : SimpleGraph (Fin 4) := + cubeGraph.quotientGraph cubeAntipodalMap + +instance : DecidableRel cubeQuotientGraph.Adj := by + intro i j; unfold cubeQuotientGraph quotientGraph; simp only; exact instDecidableAnd + +/-- The 3-cube is 3-regular. -/ +theorem cubeGraph_regular : + ∀ v : Fin 8, (Finset.univ.filter fun w => cubeGraph.Adj v w).card = 3 := by + native_decide + +/-- The 3-cube has 12 edges. -/ +theorem cubeGraph_edgeCount : + (Finset.univ.filter fun p : Fin 8 × Fin 8 => + p.1 < p.2 ∧ cubeGraph.Adj p.1 p.2).card = 12 := by + native_decide + +/-- The antipodal quotient of the 3-cube is 3-regular. -/ +theorem cubeQuotientGraph_regular : + ∀ v : Fin 4, (Finset.univ.filter fun w => cubeQuotientGraph.Adj v w).card = 3 := by + native_decide + +/-- The antipodal quotient of the 3-cube is the complete graph K₄. -/ +theorem cubeQuotient_eq_top : cubeQuotientGraph = ⊤ := by + ext u v; revert u v; native_decide + +/-! ## Sabidussi coset graph representations -/ + +section WordMachinery +variable {n k : ℕ} +private def genOrInv' (gens : Fin k → Equiv.Perm (Fin n)) (i : Fin (2 * k)) : + Equiv.Perm (Fin n) := + if h : i.val < k then gens ⟨i.val, h⟩ else (gens ⟨i.val - k, by omega⟩).symm +private def applyWord' (gens : Fin k → Equiv.Perm (Fin n)) : + List (Fin (2 * k)) → Equiv.Perm (Fin n) + | [] => Equiv.refl _ + | i :: rest => (genOrInv' gens i).trans (applyWord' gens rest) +private theorem genOrInv'_mem (gens : Fin k → Equiv.Perm (Fin n)) (i : Fin (2 * k)) : + genOrInv' gens i ∈ Subgroup.closure (Set.range gens) := by + unfold genOrInv'; split + · exact Subgroup.subset_closure ⟨_, rfl⟩ + · exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨_, rfl⟩) +private theorem applyWord'_mem (gens : Fin k → Equiv.Perm (Fin n)) + (w : List (Fin (2 * k))) : applyWord' gens w ∈ Subgroup.closure (Set.range gens) := by + induction w with + | nil => exact Subgroup.one_mem _ + | cons i rest ih => exact Subgroup.mul_mem _ ih (genOrInv'_mem gens i) +private theorem closureGraphAction {Γ : SimpleGraph (Fin n)} + (gens : Fin k → Equiv.Perm (Fin n)) + (hadj : ∀ i u v, Γ.Adj u v → Γ.Adj (gens i u) (gens i v)) + (σ : Equiv.Perm (Fin n)) (hσ : σ ∈ Subgroup.closure (Set.range gens)) + (u v : Fin n) (h : Γ.Adj u v) : Γ.Adj (σ u) (σ v) := by + refine Subgroup.closure_induction + (p := fun σ _ => ∀ u v, Γ.Adj u v → Γ.Adj (σ u) (σ v)) ?_ ?_ ?_ ?_ hσ u v h + · intro x ⟨i, hi⟩; subst hi; exact hadj i + · intro u v h; simpa + · intro x y _ _ hx hy u v h; simp only [Equiv.Perm.mul_apply]; exact hx _ _ (hy u v h) + · intro x _ hx u v h + let f : { p : Fin n × Fin n // Γ.Adj p.1 p.2 } → + { p : Fin n × Fin n // Γ.Adj p.1 p.2 } := + fun ⟨⟨a, b⟩, hab⟩ => ⟨⟨x a, x b⟩, hx a b hab⟩ + have := (Finite.surjective_of_injective (fun ⟨⟨a₁,b₁⟩,_⟩ ⟨⟨a₂,b₂⟩,_⟩ h => by + simp only [f,Subtype.mk.injEq,Prod.mk.injEq] at h + exact Subtype.ext (Prod.ext (x.injective h.1) (x.injective h.2))) + : Function.Surjective f) ⟨⟨u,v⟩,h⟩ + obtain ⟨⟨⟨a,b⟩,hab⟩,heq⟩ := this + simp only [f,Subtype.mk.injEq,Prod.mk.injEq] at heq + rw [show a = x⁻¹ u from by rw [← heq.1]; simp, + show b = x⁻¹ v from by rw [← heq.2]; simp] at hab; exact hab +end WordMachinery + +section DodecahedronSabidussi +private def dGen1Fwd : Array (Fin 20) := #[1,2,3,4,0,7,8,9,10,11,12,13,14,5,6,16,17,18,19,15] +private def dGen1Inv : Array (Fin 20) := #[4,0,1,2,3,13,14,5,6,7,8,9,10,11,12,19,15,16,17,18] +private def dGen2Fwd : Array (Fin 20) := #[0,4,13,14,5,1,2,3,11,12,18,19,15,6,7,9,10,17,16,8] +private def dGen2Inv : Array (Fin 20) := #[0,5,6,7,1,4,13,14,19,15,16,8,9,2,3,12,18,17,10,11] +private theorem dG1F_s : dGen1Fwd.size = 20 := by native_decide +private theorem dG1I_s : dGen1Inv.size = 20 := by native_decide +private theorem dG2F_s : dGen2Fwd.size = 20 := by native_decide +private theorem dG2I_s : dGen2Inv.size = 20 := by native_decide +private def dG1 : Equiv.Perm (Fin 20) where + toFun i := dGen1Fwd[i.val]'(by have := dG1F_s; omega) + invFun i := dGen1Inv[i.val]'(by have := dG1I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def dG2 : Equiv.Perm (Fin 20) where + toFun i := dGen2Fwd[i.val]'(by have := dG2F_s; omega) + invFun i := dGen2Inv[i.val]'(by have := dG2I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def dGens : Fin 2 → Equiv.Perm (Fin 20) | 0 => dG1 | 1 => dG2 +private def dGroup : Subgroup (Equiv.Perm (Fin 20)) := Subgroup.closure (Set.range dGens) +private def dWitData : Array (List (Fin 4)) := #[ + [],[0],[0,0],[2,2],[2],[0,3],[0,0,3],[0,3,0],[0,0,3,0],[0,3,0,0], + [0,0,3,0,0],[0,0,1,2],[2,2,1,2],[0,0,1],[2,2,1], + [0,3,0,0,3],[0,0,3,0,0,3],[0,0,1,2,1,2,2],[0,0,1,2,1,2],[0,0,1,2,1]] +private theorem dWitData_s : dWitData.size = 20 := by native_decide +private def dWit (v : Fin 20) : List (Fin 4) := dWitData[v.val]'(by have := dWitData_s; omega) +private theorem dWit_ok : ∀ v : Fin 20, applyWord' dGens (dWit v) 0 = v := by native_decide +private noncomputable instance : MulAction dGroup (Fin 20) := MulAction.compHom _ dGroup.subtype +private noncomputable instance : GraphAction dGroup (Fin 20) dodecahedronGraph where + adj_smul g u v h := closureGraphAction dGens + (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide)) + g.1 g.2 u v h +private noncomputable instance : MulAction.IsPretransitive dGroup (Fin 20) where + exists_smul_eq x y := ⟨⟨_, dGroup.mul_mem (applyWord'_mem dGens _) + (dGroup.inv_mem (applyWord'_mem dGens _))⟩, by + change ((applyWord' dGens (dWit x)).symm.trans (applyWord' dGens (dWit y))) x = y + simp only [Equiv.trans_apply] + rw [show (applyWord' dGens (dWit x)).symm x = 0 from by + rw [Equiv.symm_apply_eq]; exact (dWit_ok x).symm]; exact dWit_ok y⟩ + +/-- **The dodecahedron is a Sabidussi coset graph**: `Sab(A₅, C₃, D)`. -/ +noncomputable def dodecahedronSabidussiIso : + dodecahedronGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer dGroup (0 : Fin 20)) + (connectionSet dGroup dodecahedronGraph 0) (connectionSet.isConnectionSet 0) := + sabidussiIso 0 +end DodecahedronSabidussi + +section CubeSabidussi +private def cG1F : Array (Fin 8) := #[2,3,6,7,0,1,4,5] +private def cG1I : Array (Fin 8) := #[4,5,0,1,6,7,2,3] +private def cG2F : Array (Fin 8) := #[0,2,4,6,1,3,5,7] +private def cG2I : Array (Fin 8) := #[0,4,1,5,2,6,3,7] +private theorem cG1F_s : cG1F.size = 8 := by native_decide +private theorem cG1I_s : cG1I.size = 8 := by native_decide +private theorem cG2F_s : cG2F.size = 8 := by native_decide +private theorem cG2I_s : cG2I.size = 8 := by native_decide +private def cG1 : Equiv.Perm (Fin 8) where + toFun i := cG1F[i.val]'(by have := cG1F_s; omega) + invFun i := cG1I[i.val]'(by have := cG1I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def cG2 : Equiv.Perm (Fin 8) where + toFun i := cG2F[i.val]'(by have := cG2F_s; omega) + invFun i := cG2I[i.val]'(by have := cG2I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def cGens : Fin 2 → Equiv.Perm (Fin 8) | 0 => cG1 | 1 => cG2 +private def cGroup : Subgroup (Equiv.Perm (Fin 8)) := Subgroup.closure (Set.range cGens) +private def cWitData : Array (List (Fin 4)) := #[[],[0,3],[0],[0,0,3],[2],[0,0,1],[0,0],[0,0,1,2]] +private theorem cWitData_s : cWitData.size = 8 := by native_decide +private def cWit (v : Fin 8) : List (Fin 4) := cWitData[v.val]'(by have := cWitData_s; omega) +private theorem cWit_ok : ∀ v : Fin 8, applyWord' cGens (cWit v) 0 = v := by native_decide +private noncomputable instance : MulAction cGroup (Fin 8) := MulAction.compHom _ cGroup.subtype +private noncomputable instance : GraphAction cGroup (Fin 8) cubeGraph where + adj_smul g u v h := closureGraphAction cGens + (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide)) + g.1 g.2 u v h +private noncomputable instance : MulAction.IsPretransitive cGroup (Fin 8) where + exists_smul_eq x y := ⟨⟨_, cGroup.mul_mem (applyWord'_mem cGens _) + (cGroup.inv_mem (applyWord'_mem cGens _))⟩, by + change ((applyWord' cGens (cWit x)).symm.trans (applyWord' cGens (cWit y))) x = y + simp only [Equiv.trans_apply] + rw [show (applyWord' cGens (cWit x)).symm x = 0 from by + rw [Equiv.symm_apply_eq]; exact (cWit_ok x).symm]; exact cWit_ok y⟩ + +/-- **The 3-cube is a Sabidussi coset graph**: `Sab(S₄, C₃, D)`. -/ +noncomputable def cubeSabidussiIso : + cubeGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer cGroup (0 : Fin 8)) + (connectionSet cGroup cubeGraph 0) (connectionSet.isConnectionSet 0) := + sabidussiIso 0 +end CubeSabidussi + +section PetersenSabidussi +private def pG1F : Array (Fin 10) := #[2,1,7,6,3,9,5,0,4,8] +private def pG1I : Array (Fin 10) := #[7,1,0,4,8,6,3,2,9,5] +private def pG2F : Array (Fin 10) := #[3,4,0,5,6,2,9,8,7,1] +private def pG2I : Array (Fin 10) := #[2,9,5,0,1,3,4,8,7,6] +private theorem pG1F_s : pG1F.size = 10 := by native_decide +private theorem pG1I_s : pG1I.size = 10 := by native_decide +private theorem pG2F_s : pG2F.size = 10 := by native_decide +private theorem pG2I_s : pG2I.size = 10 := by native_decide +private def pG1 : Equiv.Perm (Fin 10) where + toFun i := pG1F[i.val]'(by have := pG1F_s; omega) + invFun i := pG1I[i.val]'(by have := pG1I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def pG2 : Equiv.Perm (Fin 10) where + toFun i := pG2F[i.val]'(by have := pG2F_s; omega) + invFun i := pG2I[i.val]'(by have := pG2I_s; omega) + left_inv := by native_decide + right_inv := by native_decide +private def pGens : Fin 2 → Equiv.Perm (Fin 10) | 0 => pG1 | 1 => pG2 +private def pGroup : Subgroup (Equiv.Perm (Fin 10)) := Subgroup.closure (Set.range pGens) +private def pWD : Array (List (Fin 4)) := + #[[], [1,2,3], [0], [1], [1,2], [0,3], [1,0], [2], [2,1], [0,3,0]] +private theorem pWD_s : pWD.size = 10 := by native_decide +private def pWit (v : Fin 10) : List (Fin 4) := pWD[v.val]'(by have := pWD_s; omega) +private theorem pWit_ok : + ∀ v : Fin 10, applyWord' pGens (pWit v) 0 = v := by native_decide +private noncomputable instance : MulAction pGroup (Fin 10) := MulAction.compHom _ pGroup.subtype +private noncomputable instance : GraphAction pGroup (Fin 10) petersenGraph where + adj_smul g u v h := closureGraphAction pGens + (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide)) + g.1 g.2 u v h +private noncomputable instance : MulAction.IsPretransitive pGroup (Fin 10) where + exists_smul_eq x y := + ⟨⟨_, pGroup.mul_mem (applyWord'_mem pGens _) (pGroup.inv_mem (applyWord'_mem pGens _))⟩, by + change ((applyWord' pGens (pWit x)).symm.trans (applyWord' pGens (pWit y))) x = y + simp only [Equiv.trans_apply] + rw [show (applyWord' pGens (pWit x)).symm x = 0 from by + rw [Equiv.symm_apply_eq]; exact (pWit_ok x).symm]; exact pWit_ok y⟩ + +/-- **The Petersen graph is a Sabidussi coset graph**: `Sab(S₅, S₂×S₃, D)`. -/ +noncomputable def petersenSabidussiIso : + petersenGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer pGroup (0 : Fin 10)) + (connectionSet pGroup petersenGraph 0) (connectionSet.isConnectionSet 0) := + sabidussiIso 0 +end PetersenSabidussi diff --git a/Mathlib.lean b/Mathlib.lean index af8a66d0fcb56b..9c9a4d5218833e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1,6 +1,5 @@ -module -- shake: keep-all --deprecated_module: ignore -public import Std +module -- shake: keep-all --deprecated_module: ignore public import Batteries public import Mathlib.Algebra.AddConstMap.Basic public import Mathlib.Algebra.AddConstMap.Equiv @@ -143,8 +142,8 @@ public import Mathlib.Algebra.Category.Grp.Shrink public import Mathlib.Algebra.Category.Grp.Subobject public import Mathlib.Algebra.Category.Grp.Ulift public import Mathlib.Algebra.Category.Grp.Yoneda -public import Mathlib.Algebra.Category.Grp.ZModuleEquivalence public import Mathlib.Algebra.Category.Grp.Zero +public import Mathlib.Algebra.Category.Grp.ZModuleEquivalence public import Mathlib.Algebra.Category.GrpWithZero public import Mathlib.Algebra.Category.HopfAlgCat.Basic public import Mathlib.Algebra.Category.HopfAlgCat.Monoidal @@ -428,11 +427,10 @@ public import Mathlib.Algebra.Group.Nat.TypeTags public import Mathlib.Algebra.Group.Nat.Units public import Mathlib.Algebra.Group.NatPowAssoc public import Mathlib.Algebra.Group.Opposite -public import Mathlib.Algebra.Group.PNatPowAssoc -public import Mathlib.Algebra.Group.PUnit public import Mathlib.Algebra.Group.Pi.Basic public import Mathlib.Algebra.Group.Pi.Lemmas public import Mathlib.Algebra.Group.Pi.Units +public import Mathlib.Algebra.Group.PNatPowAssoc public import Mathlib.Algebra.Group.Pointwise.Finset.Basic public import Mathlib.Algebra.Group.Pointwise.Finset.BigOperators public import Mathlib.Algebra.Group.Pointwise.Finset.Density @@ -447,6 +445,7 @@ public import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn public import Mathlib.Algebra.Group.Pointwise.Set.Scalar public import Mathlib.Algebra.Group.Pointwise.Set.Small public import Mathlib.Algebra.Group.Prod +public import Mathlib.Algebra.Group.PUnit public import Mathlib.Algebra.Group.Semiconj.Basic public import Mathlib.Algebra.Group.Semiconj.Defs public import Mathlib.Algebra.Group.Semiconj.Units @@ -721,6 +720,7 @@ public import Mathlib.Algebra.Lie.Basic public import Mathlib.Algebra.Lie.Basis public import Mathlib.Algebra.Lie.CartanCriterion public import Mathlib.Algebra.Lie.CartanExists +public import Mathlib.Algebra.Lie.CartanMatrix public import Mathlib.Algebra.Lie.CartanSubalgebra public import Mathlib.Algebra.Lie.Character public import Mathlib.Algebra.Lie.Classical @@ -809,9 +809,8 @@ public import Mathlib.Algebra.Module.LocalizedModule.Submodule public import Mathlib.Algebra.Module.MinimalAxioms public import Mathlib.Algebra.Module.NatInt public import Mathlib.Algebra.Module.Opposite -public import Mathlib.Algebra.Module.PID -public import Mathlib.Algebra.Module.PUnit public import Mathlib.Algebra.Module.Pi +public import Mathlib.Algebra.Module.PID public import Mathlib.Algebra.Module.PointwisePi public import Mathlib.Algebra.Module.Presentation.Basic public import Mathlib.Algebra.Module.Presentation.Cokernel @@ -824,6 +823,7 @@ public import Mathlib.Algebra.Module.Presentation.Tautological public import Mathlib.Algebra.Module.Presentation.Tensor public import Mathlib.Algebra.Module.Prod public import Mathlib.Algebra.Module.Projective +public import Mathlib.Algebra.Module.PUnit public import Mathlib.Algebra.Module.Rat public import Mathlib.Algebra.Module.RingHom public import Mathlib.Algebra.Module.Shrink @@ -900,10 +900,6 @@ public import Mathlib.Algebra.MvPolynomial.SchwartzZippel public import Mathlib.Algebra.MvPolynomial.Supported public import Mathlib.Algebra.MvPolynomial.Variables public import Mathlib.Algebra.NeZero -public import Mathlib.Algebra.NoZeroSMulDivisors.Basic -public import Mathlib.Algebra.NoZeroSMulDivisors.Defs -public import Mathlib.Algebra.NoZeroSMulDivisors.Pi -public import Mathlib.Algebra.NoZeroSMulDivisors.Prod public import Mathlib.Algebra.NonAssoc.LieAdmissible.Defs public import Mathlib.Algebra.NonAssoc.PreLie.Basic public import Mathlib.Algebra.Notation @@ -915,6 +911,10 @@ public import Mathlib.Algebra.Notation.Pi.Basic public import Mathlib.Algebra.Notation.Pi.Defs public import Mathlib.Algebra.Notation.Prod public import Mathlib.Algebra.Notation.Support +public import Mathlib.Algebra.NoZeroSMulDivisors.Basic +public import Mathlib.Algebra.NoZeroSMulDivisors.Defs +public import Mathlib.Algebra.NoZeroSMulDivisors.Pi +public import Mathlib.Algebra.NoZeroSMulDivisors.Prod public import Mathlib.Algebra.Opposites public import Mathlib.Algebra.Order.AbsoluteValue.Basic public import Mathlib.Algebra.Order.AbsoluteValue.Euclidean @@ -1037,6 +1037,7 @@ public import Mathlib.Algebra.Order.Interval.Set.SuccPred public import Mathlib.Algebra.Order.Invertible public import Mathlib.Algebra.Order.IsBotOne public import Mathlib.Algebra.Order.Kleene +public import Mathlib.Algebra.Order.Module.Algebra public import Mathlib.Algebra.Order.Module.Archimedean public import Mathlib.Algebra.Order.Module.Basic public import Mathlib.Algebra.Order.Module.Defs @@ -1079,10 +1080,10 @@ public import Mathlib.Algebra.Order.Nonneg.Floor public import Mathlib.Algebra.Order.Nonneg.Lattice public import Mathlib.Algebra.Order.Nonneg.Module public import Mathlib.Algebra.Order.Nonneg.Ring -public import Mathlib.Algebra.Order.PUnit public import Mathlib.Algebra.Order.Pi public import Mathlib.Algebra.Order.Positive.Field public import Mathlib.Algebra.Order.Positive.Ring +public import Mathlib.Algebra.Order.PUnit public import Mathlib.Algebra.Order.Quantale public import Mathlib.Algebra.Order.Rearrangement public import Mathlib.Algebra.Order.Ring.Abs @@ -1171,6 +1172,7 @@ public import Mathlib.Algebra.Polynomial.Eval.Irreducible public import Mathlib.Algebra.Polynomial.Eval.SMul public import Mathlib.Algebra.Polynomial.Eval.Subring public import Mathlib.Algebra.Polynomial.Expand +public import Mathlib.Algebra.Polynomial.Factors public import Mathlib.Algebra.Polynomial.FieldDivision public import Mathlib.Algebra.Polynomial.GroupRingAction public import Mathlib.Algebra.Polynomial.HasseDeriv @@ -1202,6 +1204,7 @@ public import Mathlib.Algebra.Polynomial.UnitTrinomial public import Mathlib.Algebra.PresentedMonoid.Basic public import Mathlib.Algebra.Prime.Defs public import Mathlib.Algebra.Prime.Lemmas +public import Mathlib.Algebra.QuadraticAlgebra public import Mathlib.Algebra.QuadraticAlgebra.Basic public import Mathlib.Algebra.QuadraticAlgebra.Defs public import Mathlib.Algebra.QuadraticAlgebra.NormDeterminant @@ -1265,13 +1268,13 @@ public import Mathlib.Algebra.Ring.Nat public import Mathlib.Algebra.Ring.NegOnePow public import Mathlib.Algebra.Ring.NonZeroDivisors public import Mathlib.Algebra.Ring.Opposite -public import Mathlib.Algebra.Ring.PUnit public import Mathlib.Algebra.Ring.Parity public import Mathlib.Algebra.Ring.Periodic public import Mathlib.Algebra.Ring.Pi public import Mathlib.Algebra.Ring.Pointwise.Finset public import Mathlib.Algebra.Ring.Pointwise.Set public import Mathlib.Algebra.Ring.Prod +public import Mathlib.Algebra.Ring.PUnit public import Mathlib.Algebra.Ring.Rat public import Mathlib.Algebra.Ring.Regular public import Mathlib.Algebra.Ring.Semiconj @@ -1307,9 +1310,9 @@ public import Mathlib.Algebra.SkewPolynomial.Basic public import Mathlib.Algebra.Squarefree.Basic public import Mathlib.Algebra.Star.Basic public import Mathlib.Algebra.Star.BigOperators -public import Mathlib.Algebra.Star.CHSH public import Mathlib.Algebra.Star.Center public import Mathlib.Algebra.Star.CentroidHom +public import Mathlib.Algebra.Star.CHSH public import Mathlib.Algebra.Star.Conjneg public import Mathlib.Algebra.Star.Free public import Mathlib.Algebra.Star.LinearMap @@ -1496,9 +1499,9 @@ public import Mathlib.AlgebraicTopology.DoldKan.GammaCompN public import Mathlib.AlgebraicTopology.DoldKan.Homotopies public import Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence public import Mathlib.AlgebraicTopology.DoldKan.NCompGamma -public import Mathlib.AlgebraicTopology.DoldKan.NReflectsIso public import Mathlib.AlgebraicTopology.DoldKan.Normalized public import Mathlib.AlgebraicTopology.DoldKan.Notations +public import Mathlib.AlgebraicTopology.DoldKan.NReflectsIso public import Mathlib.AlgebraicTopology.DoldKan.PInfty public import Mathlib.AlgebraicTopology.DoldKan.Projections public import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject @@ -1507,8 +1510,8 @@ public import Mathlib.AlgebraicTopology.ExtraDegeneracy public import Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup public import Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps -public import Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit public import Mathlib.AlgebraicTopology.FundamentalGroupoid.Product +public import Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected public import Mathlib.AlgebraicTopology.ModelCategory.Basic public import Mathlib.AlgebraicTopology.ModelCategory.Bifibrant @@ -1640,12 +1643,12 @@ public import Mathlib.AlgebraicTopology.TopologicalSimplex public import Mathlib.Analysis.AbsoluteValue.Equivalence public import Mathlib.Analysis.Analytic.Basic public import Mathlib.Analysis.Analytic.Binomial -public import Mathlib.Analysis.Analytic.CPolynomial -public import Mathlib.Analysis.Analytic.CPolynomialDef public import Mathlib.Analysis.Analytic.ChangeOrigin public import Mathlib.Analysis.Analytic.Composition public import Mathlib.Analysis.Analytic.Constructions public import Mathlib.Analysis.Analytic.ConvergenceRadius +public import Mathlib.Analysis.Analytic.CPolynomial +public import Mathlib.Analysis.Analytic.CPolynomialDef public import Mathlib.Analysis.Analytic.Inverse public import Mathlib.Analysis.Analytic.IsolatedZeros public import Mathlib.Analysis.Analytic.IteratedFDeriv @@ -1655,8 +1658,8 @@ public import Mathlib.Analysis.Analytic.Order public import Mathlib.Analysis.Analytic.Polynomial public import Mathlib.Analysis.Analytic.RadiusLiminf public import Mathlib.Analysis.Analytic.Uniqueness -public import Mathlib.Analysis.Analytic.WithLp public import Mathlib.Analysis.Analytic.Within +public import Mathlib.Analysis.Analytic.WithLp public import Mathlib.Analysis.AperiodicOrder.Delone.Basic public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent public import Mathlib.Analysis.Asymptotics.Completion @@ -1666,8 +1669,8 @@ public import Mathlib.Analysis.Asymptotics.Lemmas public import Mathlib.Analysis.Asymptotics.LinearGrowth public import Mathlib.Analysis.Asymptotics.SpecificAsymptotics public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay -public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.Asymptotics.Theta +public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.BoundedVariation public import Mathlib.Analysis.BoxIntegral.Basic public import Mathlib.Analysis.BoxIntegral.Box.Basic @@ -1682,50 +1685,6 @@ public import Mathlib.Analysis.BoxIntegral.Partition.Split public import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction public import Mathlib.Analysis.BoxIntegral.Partition.Tagged public import Mathlib.Analysis.BoxIntegral.UnitPartition -public import Mathlib.Analysis.CStarAlgebra.ApproximateUnit -public import Mathlib.Analysis.CStarAlgebra.Basic -public import Mathlib.Analysis.CStarAlgebra.CStarMatrix -public import Mathlib.Analysis.CStarAlgebra.Classes -public import Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital -public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary -public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap -public import Mathlib.Analysis.CStarAlgebra.ContinuousMap -public import Mathlib.Analysis.CStarAlgebra.Exponential -public import Mathlib.Analysis.CStarAlgebra.Extreme -public import Mathlib.Analysis.CStarAlgebra.Fuglede -public import Mathlib.Analysis.CStarAlgebra.GelfandDuality -public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal -public import Mathlib.Analysis.CStarAlgebra.Hom -public import Mathlib.Analysis.CStarAlgebra.Matrix -public import Mathlib.Analysis.CStarAlgebra.Module.Constructions -public import Mathlib.Analysis.CStarAlgebra.Module.Defs -public import Mathlib.Analysis.CStarAlgebra.Module.Synonym -public import Mathlib.Analysis.CStarAlgebra.Multiplier -public import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap -public import Mathlib.Analysis.CStarAlgebra.Projection -public import Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart -public import Mathlib.Analysis.CStarAlgebra.Spectrum -public import Mathlib.Analysis.CStarAlgebra.Unitary.Connected -public import Mathlib.Analysis.CStarAlgebra.Unitary.Maps -public import Mathlib.Analysis.CStarAlgebra.Unitary.Span -public import Mathlib.Analysis.CStarAlgebra.Unitization -public import Mathlib.Analysis.CStarAlgebra.lpSpace public import Mathlib.Analysis.Calculus.AbsolutelyMonotone public import Mathlib.Analysis.Calculus.AddTorsor.AffineMap public import Mathlib.Analysis.Calculus.AddTorsor.Coord @@ -1739,21 +1698,20 @@ public import Mathlib.Analysis.Calculus.Conformal.InnerProduct public import Mathlib.Analysis.Calculus.Conformal.NormedSpace public import Mathlib.Analysis.Calculus.ContDiff.Basic public import Mathlib.Analysis.Calculus.ContDiff.Bounds -public import Mathlib.Analysis.Calculus.ContDiff.CPolynomial public import Mathlib.Analysis.Calculus.ContDiff.Comp public import Mathlib.Analysis.Calculus.ContDiff.Convolution +public import Mathlib.Analysis.Calculus.ContDiff.CPolynomial public import Mathlib.Analysis.Calculus.ContDiff.Defs public import Mathlib.Analysis.Calculus.ContDiff.Deriv -public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries public import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension +public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries public import Mathlib.Analysis.Calculus.ContDiff.Operations public import Mathlib.Analysis.Calculus.ContDiff.Polynomial public import Mathlib.Analysis.Calculus.ContDiff.RCLike public import Mathlib.Analysis.Calculus.ContDiff.RestrictScalars public import Mathlib.Analysis.Calculus.ContDiff.WithLp public import Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise -public import Mathlib.Analysis.Calculus.DSlope public import Mathlib.Analysis.Calculus.Darboux public import Mathlib.Analysis.Calculus.Deriv.Abs public import Mathlib.Analysis.Calculus.Deriv.Add @@ -1779,6 +1737,7 @@ public import Mathlib.Analysis.Calculus.DerivativeTest public import Mathlib.Analysis.Calculus.DiffContOnCl public import Mathlib.Analysis.Calculus.DifferentialForm.Basic public import Mathlib.Analysis.Calculus.DifferentialForm.VectorField +public import Mathlib.Analysis.Calculus.DSlope public import Mathlib.Analysis.Calculus.FDeriv.Add public import Mathlib.Analysis.Calculus.FDeriv.Affine public import Mathlib.Analysis.Calculus.FDeriv.Analytic @@ -1824,8 +1783,8 @@ public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs public import Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas public import Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow -public import Mathlib.Analysis.Calculus.LHopital public import Mathlib.Analysis.Calculus.LagrangeMultipliers +public import Mathlib.Analysis.Calculus.LHopital public import Mathlib.Analysis.Calculus.LineDeriv.Basic public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts public import Mathlib.Analysis.Calculus.LineDeriv.Measurable @@ -1842,6 +1801,7 @@ public import Mathlib.Analysis.Calculus.ParametricIntegral public import Mathlib.Analysis.Calculus.ParametricIntervalIntegral public import Mathlib.Analysis.Calculus.Rademacher public import Mathlib.Analysis.Calculus.SmoothSeries +public import Mathlib.Analysis.Calculus.TangentCone public import Mathlib.Analysis.Calculus.TangentCone.Basic public import Mathlib.Analysis.Calculus.TangentCone.Defs public import Mathlib.Analysis.Calculus.TangentCone.DimOne @@ -1896,8 +1856,8 @@ public import Mathlib.Analysis.Complex.Polynomial.Basic public import Mathlib.Analysis.Complex.Polynomial.GaussLucas public import Mathlib.Analysis.Complex.Polynomial.UnitTrinomial public import Mathlib.Analysis.Complex.Positivity -public import Mathlib.Analysis.Complex.ReImTopology public import Mathlib.Analysis.Complex.RealDeriv +public import Mathlib.Analysis.Complex.ReImTopology public import Mathlib.Analysis.Complex.RemovableSingularity public import Mathlib.Analysis.Complex.RiemannMapping public import Mathlib.Analysis.Complex.Schwarz @@ -1993,6 +1953,50 @@ public import Mathlib.Analysis.Convex.TotallyBounded public import Mathlib.Analysis.Convex.Uniform public import Mathlib.Analysis.Convex.Visible public import Mathlib.Analysis.Convolution +public import Mathlib.Analysis.CStarAlgebra.ApproximateUnit +public import Mathlib.Analysis.CStarAlgebra.Basic +public import Mathlib.Analysis.CStarAlgebra.Classes +public import Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary +public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap +public import Mathlib.Analysis.CStarAlgebra.ContinuousMap +public import Mathlib.Analysis.CStarAlgebra.CStarMatrix +public import Mathlib.Analysis.CStarAlgebra.Exponential +public import Mathlib.Analysis.CStarAlgebra.Extreme +public import Mathlib.Analysis.CStarAlgebra.Fuglede +public import Mathlib.Analysis.CStarAlgebra.GelfandDuality +public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal +public import Mathlib.Analysis.CStarAlgebra.Hom +public import Mathlib.Analysis.CStarAlgebra.lpSpace +public import Mathlib.Analysis.CStarAlgebra.Matrix +public import Mathlib.Analysis.CStarAlgebra.Module.Constructions +public import Mathlib.Analysis.CStarAlgebra.Module.Defs +public import Mathlib.Analysis.CStarAlgebra.Module.Synonym +public import Mathlib.Analysis.CStarAlgebra.Multiplier +public import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap +public import Mathlib.Analysis.CStarAlgebra.Projection +public import Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart +public import Mathlib.Analysis.CStarAlgebra.Spectrum +public import Mathlib.Analysis.CStarAlgebra.Unitary.Connected +public import Mathlib.Analysis.CStarAlgebra.Unitary.Maps +public import Mathlib.Analysis.CStarAlgebra.Unitary.Span +public import Mathlib.Analysis.CStarAlgebra.Unitization public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff public import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn public import Mathlib.Analysis.Distribution.DerivNotation @@ -2043,6 +2047,7 @@ public import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic public import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions public import Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl public import Mathlib.Analysis.InnerProductSpace.JointEigenspace +public import Mathlib.Analysis.InnerProductSpace.l2Space public import Mathlib.Analysis.InnerProductSpace.Laplacian public import Mathlib.Analysis.InnerProductSpace.LaxMilgram public import Mathlib.Analysis.InnerProductSpace.LinearMap @@ -2075,7 +2080,6 @@ public import Mathlib.Analysis.InnerProductSpace.TensorProduct public import Mathlib.Analysis.InnerProductSpace.Trace public import Mathlib.Analysis.InnerProductSpace.TwoDim public import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology -public import Mathlib.Analysis.InnerProductSpace.l2Space public import Mathlib.Analysis.LConvolution public import Mathlib.Analysis.LocallyConvex.AbsConvex public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen @@ -2095,6 +2099,7 @@ public import Mathlib.Analysis.LocallyConvex.WeakDual public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology public import Mathlib.Analysis.LocallyConvex.WeakSpace public import Mathlib.Analysis.LocallyConvex.WithSeminorms +public import Mathlib.Analysis.Matrix public import Mathlib.Analysis.Matrix.Hermitian public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus public import Mathlib.Analysis.Matrix.LDL @@ -2171,10 +2176,10 @@ public import Mathlib.Analysis.Normed.Group.Pointwise public import Mathlib.Analysis.Normed.Group.Quotient public import Mathlib.Analysis.Normed.Group.Rat public import Mathlib.Analysis.Normed.Group.Real +public import Mathlib.Analysis.Normed.Group.Seminorm public import Mathlib.Analysis.Normed.Group.SemiNormedGrp public import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion public import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels -public import Mathlib.Analysis.Normed.Group.Seminorm public import Mathlib.Analysis.Normed.Group.SeparationQuotient public import Mathlib.Analysis.Normed.Group.Subgroup public import Mathlib.Analysis.Normed.Group.Submodule @@ -2184,14 +2189,14 @@ public import Mathlib.Analysis.Normed.Group.Uniform public import Mathlib.Analysis.Normed.Group.ZeroAtInfty public import Mathlib.Analysis.Normed.Lp.Finsupp public import Mathlib.Analysis.Normed.Lp.LpEquiv +public import Mathlib.Analysis.Normed.Lp.lpHolder +public import Mathlib.Analysis.Normed.Lp.lpSpace public import Mathlib.Analysis.Normed.Lp.Matrix public import Mathlib.Analysis.Normed.Lp.MeasurableSpace public import Mathlib.Analysis.Normed.Lp.PiLp public import Mathlib.Analysis.Normed.Lp.ProdLp public import Mathlib.Analysis.Normed.Lp.SmoothApprox public import Mathlib.Analysis.Normed.Lp.WithLp -public import Mathlib.Analysis.Normed.Lp.lpHolder -public import Mathlib.Analysis.Normed.Lp.lpSpace public import Mathlib.Analysis.Normed.Module.Alternating.Basic public import Mathlib.Analysis.Normed.Module.Alternating.Curry public import Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin @@ -2208,6 +2213,7 @@ public import Mathlib.Analysis.Normed.Module.ContinuousInverse public import Mathlib.Analysis.Normed.Module.Convex public import Mathlib.Analysis.Normed.Module.DoubleDual public import Mathlib.Analysis.Normed.Module.Dual +public import Mathlib.Analysis.Normed.Module.ENormedSpace public import Mathlib.Analysis.Normed.Module.Extr public import Mathlib.Analysis.Normed.Module.FiniteDimension public import Mathlib.Analysis.Normed.Module.HahnBanach @@ -2218,10 +2224,10 @@ public import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn public import Mathlib.Analysis.Normed.Module.Normalize public import Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm public import Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm +public import Mathlib.Analysis.Normed.Module.Ray public import Mathlib.Analysis.Normed.Module.RCLike.Basic public import Mathlib.Analysis.Normed.Module.RCLike.Extend public import Mathlib.Analysis.Normed.Module.RCLike.Real -public import Mathlib.Analysis.Normed.Module.Ray public import Mathlib.Analysis.Normed.Module.RieszLemma public import Mathlib.Analysis.Normed.Module.Shrink public import Mathlib.Analysis.Normed.Module.Span @@ -2274,12 +2280,29 @@ public import Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded public import Mathlib.Analysis.Normed.Unbundled.SeminormFromConst public import Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm public import Mathlib.Analysis.Normed.Unbundled.SpectralNorm +public import Mathlib.Analysis.NormedSpace.Alternating.Basic +public import Mathlib.Analysis.NormedSpace.Alternating.Curry +public import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin +public import Mathlib.Analysis.NormedSpace.Connected +public import Mathlib.Analysis.NormedSpace.ENormedSpace +public import Mathlib.Analysis.NormedSpace.Extr public import Mathlib.Analysis.NormedSpace.FunctionSeries +public import Mathlib.Analysis.NormedSpace.HahnBanach.Extension +public import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual +public import Mathlib.Analysis.NormedSpace.HahnBanach.Separation +public import Mathlib.Analysis.NormedSpace.MStructure +public import Mathlib.Analysis.NormedSpace.Multilinear.Basic +public import Mathlib.Analysis.NormedSpace.Multilinear.Curry +public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn +public import Mathlib.Analysis.NormedSpace.Normalize public import Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness public import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm public import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod +public import Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm +public import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm public import Mathlib.Analysis.NormedSpace.RCLike public import Mathlib.Analysis.NormedSpace.Real +public import Mathlib.Analysis.NormedSpace.RieszLemma public import Mathlib.Analysis.ODE.Basic public import Mathlib.Analysis.ODE.DiscreteGronwall public import Mathlib.Analysis.ODE.ExistUnique @@ -2287,8 +2310,6 @@ public import Mathlib.Analysis.ODE.Gronwall public import Mathlib.Analysis.ODE.PicardLindelof public import Mathlib.Analysis.ODE.Transform public import Mathlib.Analysis.Oscillation -public import Mathlib.Analysis.PSeries -public import Mathlib.Analysis.PSeriesComplex public import Mathlib.Analysis.Polynomial.Basic public import Mathlib.Analysis.Polynomial.CauchyBound public import Mathlib.Analysis.Polynomial.Factorization @@ -2296,7 +2317,10 @@ public import Mathlib.Analysis.Polynomial.Fourier public import Mathlib.Analysis.Polynomial.MahlerMeasure public import Mathlib.Analysis.Polynomial.Norm public import Mathlib.Analysis.Polynomial.Order +public import Mathlib.Analysis.PSeries +public import Mathlib.Analysis.PSeriesComplex public import Mathlib.Analysis.Quaternion +public import Mathlib.Analysis.Rat.NatSqrt.Real public import Mathlib.Analysis.RCLike.Basic public import Mathlib.Analysis.RCLike.BoundedContinuous public import Mathlib.Analysis.RCLike.ContinuousMap @@ -2305,7 +2329,6 @@ public import Mathlib.Analysis.RCLike.Inner public import Mathlib.Analysis.RCLike.Lemmas public import Mathlib.Analysis.RCLike.Sqrt public import Mathlib.Analysis.RCLike.TangentCone -public import Mathlib.Analysis.Rat.NatSqrt.Real public import Mathlib.Analysis.Real.Cardinality public import Mathlib.Analysis.Real.Hyperreal public import Mathlib.Analysis.Real.OfDigits @@ -2335,6 +2358,7 @@ public import Mathlib.Analysis.SpecialFunctions.Complex.Log public import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds public import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs +public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic @@ -2401,6 +2425,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan public import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal @@ -2535,8 +2560,8 @@ public import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete public import Mathlib.CategoryTheory.Bicategory.Functor.Oplax public import Mathlib.CategoryTheory.Bicategory.Functor.Prelax public import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor -public import Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor public import Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary +public import Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor public import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax public import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax public import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo @@ -2591,9 +2616,19 @@ public import Mathlib.CategoryTheory.Center.Linear public import Mathlib.CategoryTheory.Center.Localization public import Mathlib.CategoryTheory.Center.NegOnePow public import Mathlib.CategoryTheory.Center.Preadditive +public import Mathlib.CategoryTheory.Closed.Cartesian +public import Mathlib.CategoryTheory.Closed.Enrichment +public import Mathlib.CategoryTheory.Closed.Functor +public import Mathlib.CategoryTheory.Closed.FunctorCategory.Basic +public import Mathlib.CategoryTheory.Closed.FunctorCategory.Complete +public import Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid +public import Mathlib.CategoryTheory.Closed.FunctorToTypes +public import Mathlib.CategoryTheory.Closed.Ideal +public import Mathlib.CategoryTheory.Closed.Monoidal +public import Mathlib.CategoryTheory.Closed.Types +public import Mathlib.CategoryTheory.Closed.Zero public import Mathlib.CategoryTheory.CodiscreteCategory public import Mathlib.CategoryTheory.CofilteredSystem -public import Mathlib.CategoryTheory.CommSq public import Mathlib.CategoryTheory.Comma.Arrow public import Mathlib.CategoryTheory.Comma.Basic public import Mathlib.CategoryTheory.Comma.CardinalArrow @@ -2611,6 +2646,7 @@ public import Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap public import Mathlib.CategoryTheory.Comma.StructuredArrow.Final public import Mathlib.CategoryTheory.Comma.StructuredArrow.Functor public import Mathlib.CategoryTheory.Comma.StructuredArrow.Small +public import Mathlib.CategoryTheory.CommSq public import Mathlib.CategoryTheory.ComposableArrows.Basic public import Mathlib.CategoryTheory.ComposableArrows.Four public import Mathlib.CategoryTheory.ComposableArrows.One @@ -2648,6 +2684,7 @@ public import Mathlib.CategoryTheory.EffectiveEpi.Coproduct public import Mathlib.CategoryTheory.EffectiveEpi.Enough public import Mathlib.CategoryTheory.EffectiveEpi.Extensive public import Mathlib.CategoryTheory.EffectiveEpi.Preserves +public import Mathlib.CategoryTheory.EffectiveEpi.RegularEpi public import Mathlib.CategoryTheory.Elements public import Mathlib.CategoryTheory.Elementwise public import Mathlib.CategoryTheory.Endofunctor.Algebra @@ -2849,7 +2886,6 @@ public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal public import Mathlib.CategoryTheory.Limits.FunctorToTypes public import Mathlib.CategoryTheory.Limits.HasLimits -public import Mathlib.CategoryTheory.Limits.IndYoneda public import Mathlib.CategoryTheory.Limits.Indization.Category public import Mathlib.CategoryTheory.Limits.Indization.Equalizers public import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits @@ -2857,6 +2893,7 @@ public import Mathlib.CategoryTheory.Limits.Indization.IndObject public import Mathlib.CategoryTheory.Limits.Indization.LocallySmall public import Mathlib.CategoryTheory.Limits.Indization.ParallelPair public import Mathlib.CategoryTheory.Limits.Indization.Products +public import Mathlib.CategoryTheory.Limits.IndYoneda public import Mathlib.CategoryTheory.Limits.IsConnected public import Mathlib.CategoryTheory.Limits.IsLimit public import Mathlib.CategoryTheory.Limits.Lattice @@ -2950,11 +2987,11 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback +public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels -public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone @@ -2977,9 +3014,9 @@ public import Mathlib.CategoryTheory.Limits.Sifted public import Mathlib.CategoryTheory.Limits.Skeleton public import Mathlib.CategoryTheory.Limits.SmallComplete public import Mathlib.CategoryTheory.Limits.Types.Coequalizers +public import Mathlib.CategoryTheory.Limits.Types.Colimits public import Mathlib.CategoryTheory.Limits.Types.ColimitType public import Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered -public import Mathlib.CategoryTheory.Limits.Types.Colimits public import Mathlib.CategoryTheory.Limits.Types.Coproducts public import Mathlib.CategoryTheory.Limits.Types.End public import Mathlib.CategoryTheory.Limits.Types.Equalizers @@ -2991,6 +3028,7 @@ public import Mathlib.CategoryTheory.Limits.Types.Multiequalizer public import Mathlib.CategoryTheory.Limits.Types.Products public import Mathlib.CategoryTheory.Limits.Types.Pullbacks public import Mathlib.CategoryTheory.Limits.Types.Pushouts +public import Mathlib.CategoryTheory.Limits.Types.Shapes public import Mathlib.CategoryTheory.Limits.Types.Yoneda public import Mathlib.CategoryTheory.Limits.Unit public import Mathlib.CategoryTheory.Limits.VanKampen @@ -3027,6 +3065,7 @@ public import Mathlib.CategoryTheory.Localization.HomEquiv public import Mathlib.CategoryTheory.Localization.Linear public import Mathlib.CategoryTheory.Localization.LocalizerMorphism public import Mathlib.CategoryTheory.Localization.LocallySmall +public import Mathlib.CategoryTheory.Localization.Monoidal public import Mathlib.CategoryTheory.Localization.Monoidal.Basic public import Mathlib.CategoryTheory.Localization.Monoidal.Braided public import Mathlib.CategoryTheory.Localization.Monoidal.Functor @@ -3082,8 +3121,8 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ public import Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory public import Mathlib.CategoryTheory.Monoidal.Cartesian.Grp -public import Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits public import Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ +public import Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits public import Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ @@ -3228,17 +3267,16 @@ public import Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive public import Mathlib.CategoryTheory.ObjectProperty.SiteLocal public import Mathlib.CategoryTheory.ObjectProperty.Small public import Mathlib.CategoryTheory.Opposites -public import Mathlib.CategoryTheory.PEmpty -public import Mathlib.CategoryTheory.PUnit public import Mathlib.CategoryTheory.PathCategory.Basic public import Mathlib.CategoryTheory.PathCategory.MorphismProperty +public import Mathlib.CategoryTheory.PEmpty public import Mathlib.CategoryTheory.Pi.Basic public import Mathlib.CategoryTheory.Pi.Monoidal public import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor public import Mathlib.CategoryTheory.Preadditive.Basic public import Mathlib.CategoryTheory.Preadditive.Biproducts -public import Mathlib.CategoryTheory.Preadditive.CommGrp_ public import Mathlib.CategoryTheory.Preadditive.Comma +public import Mathlib.CategoryTheory.Preadditive.CommGrp_ public import Mathlib.CategoryTheory.Preadditive.EilenbergMoore public import Mathlib.CategoryTheory.Preadditive.EndoFunctor public import Mathlib.CategoryTheory.Preadditive.FunctorCategory @@ -3288,6 +3326,7 @@ public import Mathlib.CategoryTheory.Products.Basic public import Mathlib.CategoryTheory.Products.Bifunctor public import Mathlib.CategoryTheory.Products.Unitor public import Mathlib.CategoryTheory.Profunctor.Basic +public import Mathlib.CategoryTheory.PUnit public import Mathlib.CategoryTheory.Quotient public import Mathlib.CategoryTheory.Quotient.Linear public import Mathlib.CategoryTheory.Quotient.LocallySmall @@ -3306,9 +3345,9 @@ public import Mathlib.CategoryTheory.Shift.Localization public import Mathlib.CategoryTheory.Shift.Opposite public import Mathlib.CategoryTheory.Shift.Pullback public import Mathlib.CategoryTheory.Shift.Quotient -public import Mathlib.CategoryTheory.Shift.ShiftSequence public import Mathlib.CategoryTheory.Shift.ShiftedHom public import Mathlib.CategoryTheory.Shift.ShiftedHomOpposite +public import Mathlib.CategoryTheory.Shift.ShiftSequence public import Mathlib.CategoryTheory.Shift.SingleFunctors public import Mathlib.CategoryTheory.Shift.SingleFunctorsLift public import Mathlib.CategoryTheory.Shift.Twist @@ -3343,9 +3382,9 @@ public import Mathlib.CategoryTheory.Sites.ConcreteSheafification public import Mathlib.CategoryTheory.Sites.ConstantSheaf public import Mathlib.CategoryTheory.Sites.Continuous public import Mathlib.CategoryTheory.Sites.CoproductSheafCondition +public import Mathlib.CategoryTheory.Sites.Coverage public import Mathlib.CategoryTheory.Sites.CoverLifting public import Mathlib.CategoryTheory.Sites.CoverPreserving -public import Mathlib.CategoryTheory.Sites.Coverage public import Mathlib.CategoryTheory.Sites.CoversTop public import Mathlib.CategoryTheory.Sites.CoversTop.Basic public import Mathlib.CategoryTheory.Sites.CoversTop.Over @@ -3379,12 +3418,12 @@ public import Mathlib.CategoryTheory.Sites.IsSheafFor public import Mathlib.CategoryTheory.Sites.JointlySurjective public import Mathlib.CategoryTheory.Sites.LeftExact public import Mathlib.CategoryTheory.Sites.Limits -public import Mathlib.CategoryTheory.Sites.LocalProperties public import Mathlib.CategoryTheory.Sites.Localization public import Mathlib.CategoryTheory.Sites.LocallyBijective public import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful public import Mathlib.CategoryTheory.Sites.LocallyInjective public import Mathlib.CategoryTheory.Sites.LocallySurjective +public import Mathlib.CategoryTheory.Sites.LocalProperties public import Mathlib.CategoryTheory.Sites.MayerVietorisSquare public import Mathlib.CategoryTheory.Sites.Monoidal public import Mathlib.CategoryTheory.Sites.MorphismProperty @@ -3419,8 +3458,8 @@ public import Mathlib.CategoryTheory.Sites.SheafCohomology.Basic public import Mathlib.CategoryTheory.Sites.SheafCohomology.Cech public import Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris public import Mathlib.CategoryTheory.Sites.SheafHom -public import Mathlib.CategoryTheory.Sites.SheafOfTypes public import Mathlib.CategoryTheory.Sites.Sheafification +public import Mathlib.CategoryTheory.Sites.SheafOfTypes public import Mathlib.CategoryTheory.Sites.Sieves public import Mathlib.CategoryTheory.Sites.Spaces public import Mathlib.CategoryTheory.Sites.Subcanonical @@ -3462,6 +3501,13 @@ public import Mathlib.CategoryTheory.Subobject.NoetherianObject public import Mathlib.CategoryTheory.Subobject.Presheaf public import Mathlib.CategoryTheory.Subobject.Types public import Mathlib.CategoryTheory.Subobject.WellPowered +public import Mathlib.CategoryTheory.Subpresheaf.Basic +public import Mathlib.CategoryTheory.Subpresheaf.Equalizer +public import Mathlib.CategoryTheory.Subpresheaf.Finite +public import Mathlib.CategoryTheory.Subpresheaf.Image +public import Mathlib.CategoryTheory.Subpresheaf.OfSection +public import Mathlib.CategoryTheory.Subpresheaf.Sieves +public import Mathlib.CategoryTheory.Subpresheaf.Subobject public import Mathlib.CategoryTheory.Subterminal public import Mathlib.CategoryTheory.Sums.Associator public import Mathlib.CategoryTheory.Sums.Basic @@ -3487,6 +3533,8 @@ public import Mathlib.CategoryTheory.Triangulated.Pretriangulated public import Mathlib.CategoryTheory.Triangulated.Rotate public import Mathlib.CategoryTheory.Triangulated.SpectralObject public import Mathlib.CategoryTheory.Triangulated.Subcategory +public import Mathlib.CategoryTheory.Triangulated.TriangleShift +public import Mathlib.CategoryTheory.Triangulated.Triangulated public import Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic public import Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc @@ -3495,8 +3543,6 @@ public import Mathlib.CategoryTheory.Triangulated.TStructure.Induced public import Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE -public import Mathlib.CategoryTheory.Triangulated.TriangleShift -public import Mathlib.CategoryTheory.Triangulated.Triangulated public import Mathlib.CategoryTheory.Triangulated.WeakKernels public import Mathlib.CategoryTheory.Triangulated.Yoneda public import Mathlib.CategoryTheory.Types.Basic @@ -3521,9 +3567,9 @@ public import Mathlib.Combinatorics.Additive.Corner.Roth public import Mathlib.Combinatorics.Additive.CovBySMul public import Mathlib.Combinatorics.Additive.Dissociation public import Mathlib.Combinatorics.Additive.DoublingConst -public import Mathlib.Combinatorics.Additive.ETransform public import Mathlib.Combinatorics.Additive.Energy public import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv +public import Mathlib.Combinatorics.Additive.ETransform public import Mathlib.Combinatorics.Additive.FreimanHom public import Mathlib.Combinatorics.Additive.PluenneckeRuzsa public import Mathlib.Combinatorics.Additive.Randomisation @@ -3548,6 +3594,7 @@ public import Mathlib.Combinatorics.Enumerative.DoubleCounting public import Mathlib.Combinatorics.Enumerative.DyckWord public import Mathlib.Combinatorics.Enumerative.IncidenceAlgebra public import Mathlib.Combinatorics.Enumerative.InclusionExclusion +public import Mathlib.Combinatorics.Enumerative.Partition public import Mathlib.Combinatorics.Enumerative.Partition.Basic public import Mathlib.Combinatorics.Enumerative.Partition.GenFun public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher @@ -3614,6 +3661,7 @@ public import Mathlib.Combinatorics.SetFamily.KruskalKatona public import Mathlib.Combinatorics.SetFamily.LYM public import Mathlib.Combinatorics.SetFamily.Shadow public import Mathlib.Combinatorics.SetFamily.Shatter +public import Mathlib.Combinatorics.SimpleGraph.Action public import Mathlib.Combinatorics.SimpleGraph.Acyclic public import Mathlib.Combinatorics.SimpleGraph.AdjMatrix public import Mathlib.Combinatorics.SimpleGraph.Basic @@ -3636,6 +3684,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Combinatorics.SimpleGraph.CosetGraph public import Mathlib.Combinatorics.SimpleGraph.CycleGraph public import Mathlib.Combinatorics.SimpleGraph.Dart public import Mathlib.Combinatorics.SimpleGraph.DegreeSum @@ -3666,6 +3715,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Operations public import Mathlib.Combinatorics.SimpleGraph.Partition public import Mathlib.Combinatorics.SimpleGraph.Paths public import Mathlib.Combinatorics.SimpleGraph.Prod +public import Mathlib.Combinatorics.SimpleGraph.QuotientGraph public import Mathlib.Combinatorics.SimpleGraph.Regularity.Bound public import Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk public import Mathlib.Combinatorics.SimpleGraph.Regularity.Energy @@ -3673,10 +3723,12 @@ public import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise public import Mathlib.Combinatorics.SimpleGraph.Regularity.Increment public import Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +public import Mathlib.Combinatorics.SimpleGraph.Representation public import Mathlib.Combinatorics.SimpleGraph.Star public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular public import Mathlib.Combinatorics.SimpleGraph.Subgraph public import Mathlib.Combinatorics.SimpleGraph.Sum +public import Mathlib.Combinatorics.SimpleGraph.Symmetric public import Mathlib.Combinatorics.SimpleGraph.Trails public import Mathlib.Combinatorics.SimpleGraph.Triangle.Basic public import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting @@ -3686,6 +3738,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Tutte public import Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic public import Mathlib.Combinatorics.SimpleGraph.UniversalVerts public import Mathlib.Combinatorics.SimpleGraph.VertexCover +public import Mathlib.Combinatorics.SimpleGraph.Walk public import Mathlib.Combinatorics.SimpleGraph.Walk.Basic public import Mathlib.Combinatorics.SimpleGraph.Walk.Chord public import Mathlib.Combinatorics.SimpleGraph.Walk.Counting @@ -3728,10 +3781,10 @@ public import Mathlib.Computability.RecursiveIn public import Mathlib.Computability.Reduce public import Mathlib.Computability.RegularExpressions public import Mathlib.Computability.StateTransition +public import Mathlib.Computability.Tape public import Mathlib.Computability.TMComputable public import Mathlib.Computability.TMConfig public import Mathlib.Computability.TMToPartrec -public import Mathlib.Computability.Tape public import Mathlib.Computability.TuringDegree public import Mathlib.Computability.TuringMachine public import Mathlib.Computability.TuringMachine.Computable @@ -3802,6 +3855,7 @@ public import Mathlib.Control.ULiftable public import Mathlib.Data.Analysis.Filter public import Mathlib.Data.Analysis.Topology public import Mathlib.Data.Array.Defs +public import Mathlib.Data.Array.Extract public import Mathlib.Data.BitVec public import Mathlib.Data.Bool.AllAny public import Mathlib.Data.Bool.Basic @@ -3832,6 +3886,11 @@ public import Mathlib.Data.DFinsupp.Small public import Mathlib.Data.DFinsupp.Submonoid public import Mathlib.Data.DFinsupp.WellFounded public import Mathlib.Data.DList.Instances +public import Mathlib.Data.ENat.Basic +public import Mathlib.Data.ENat.BigOperators +public import Mathlib.Data.ENat.Defs +public import Mathlib.Data.ENat.Lattice +public import Mathlib.Data.ENat.Pow public import Mathlib.Data.ENNReal.Action public import Mathlib.Data.ENNReal.Basic public import Mathlib.Data.ENNReal.BigOperators @@ -3840,16 +3899,10 @@ public import Mathlib.Data.ENNReal.Inv public import Mathlib.Data.ENNReal.Lemmas public import Mathlib.Data.ENNReal.Operations public import Mathlib.Data.ENNReal.Real -public import Mathlib.Data.ENat.Basic -public import Mathlib.Data.ENat.BigOperators -public import Mathlib.Data.ENat.Defs -public import Mathlib.Data.ENat.Lattice -public import Mathlib.Data.ENat.Pow +public import Mathlib.Data.Erased public import Mathlib.Data.EReal.Basic public import Mathlib.Data.EReal.Inv public import Mathlib.Data.EReal.Operations -public import Mathlib.Data.Erased -public import Mathlib.Data.FP.Basic public import Mathlib.Data.Fin.Basic public import Mathlib.Data.Fin.Embedding public import Mathlib.Data.Fin.Fin2 @@ -3916,19 +3969,19 @@ public import Mathlib.Data.Finset.NatDivisors public import Mathlib.Data.Finset.NoncommProd public import Mathlib.Data.Finset.Option public import Mathlib.Data.Finset.Order -public import Mathlib.Data.Finset.PImage public import Mathlib.Data.Finset.Pairwise public import Mathlib.Data.Finset.Pi -public import Mathlib.Data.Finset.PiInduction public import Mathlib.Data.Finset.Piecewise +public import Mathlib.Data.Finset.PiInduction +public import Mathlib.Data.Finset.PImage public import Mathlib.Data.Finset.Powerset public import Mathlib.Data.Finset.Preimage public import Mathlib.Data.Finset.Prod public import Mathlib.Data.Finset.Range public import Mathlib.Data.Finset.SDiff -public import Mathlib.Data.Finset.SMulAntidiagonal public import Mathlib.Data.Finset.Sigma public import Mathlib.Data.Finset.Slice +public import Mathlib.Data.Finset.SMulAntidiagonal public import Mathlib.Data.Finset.Sort public import Mathlib.Data.Finset.Sum public import Mathlib.Data.Finset.Sups @@ -3955,13 +4008,13 @@ public import Mathlib.Data.Finsupp.NeLocus public import Mathlib.Data.Finsupp.Notation public import Mathlib.Data.Finsupp.Option public import Mathlib.Data.Finsupp.Order -public import Mathlib.Data.Finsupp.PWO public import Mathlib.Data.Finsupp.Pointwise public import Mathlib.Data.Finsupp.PointwiseSMul -public import Mathlib.Data.Finsupp.SMul -public import Mathlib.Data.Finsupp.SMulWithZero +public import Mathlib.Data.Finsupp.PWO public import Mathlib.Data.Finsupp.Sigma public import Mathlib.Data.Finsupp.Single +public import Mathlib.Data.Finsupp.SMul +public import Mathlib.Data.Finsupp.SMulWithZero public import Mathlib.Data.Finsupp.ToDFinsupp public import Mathlib.Data.Finsupp.Weight public import Mathlib.Data.Finsupp.WellFounded @@ -3993,6 +4046,7 @@ public import Mathlib.Data.Fintype.Sum public import Mathlib.Data.Fintype.Units public import Mathlib.Data.Fintype.Vector public import Mathlib.Data.Fintype.WithTopBot +public import Mathlib.Data.FP.Basic public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.FunLike.Embedding public import Mathlib.Data.FunLike.Equiv @@ -4060,6 +4114,7 @@ public import Mathlib.Data.List.Indexes public import Mathlib.Data.List.Induction public import Mathlib.Data.List.Infix public import Mathlib.Data.List.InsertIdx +public import Mathlib.Data.List.InsertNth public import Mathlib.Data.List.Intervals public import Mathlib.Data.List.Iterate public import Mathlib.Data.List.Lattice @@ -4073,8 +4128,8 @@ public import Mathlib.Data.List.Monad public import Mathlib.Data.List.NatAntidiagonal public import Mathlib.Data.List.Nodup public import Mathlib.Data.List.NodupEquivFin -public import Mathlib.Data.List.OfFn public import Mathlib.Data.List.OffDiag +public import Mathlib.Data.List.OfFn public import Mathlib.Data.List.Pairwise public import Mathlib.Data.List.Palindrome public import Mathlib.Data.List.PeriodicityLemma @@ -4097,9 +4152,9 @@ public import Mathlib.Data.List.SplitLengths public import Mathlib.Data.List.SplitOn public import Mathlib.Data.List.Sublists public import Mathlib.Data.List.Sym -public import Mathlib.Data.List.TFAE public import Mathlib.Data.List.TakeDrop public import Mathlib.Data.List.TakeWhile +public import Mathlib.Data.List.TFAE public import Mathlib.Data.List.ToFinsupp public import Mathlib.Data.List.Triplewise public import Mathlib.Data.List.Zip @@ -4112,8 +4167,8 @@ public import Mathlib.Data.Matrix.Block public import Mathlib.Data.Matrix.Cartan public import Mathlib.Data.Matrix.ColumnRowPartitioned public import Mathlib.Data.Matrix.Composition -public import Mathlib.Data.Matrix.DMatrix public import Mathlib.Data.Matrix.Diagonal +public import Mathlib.Data.Matrix.DMatrix public import Mathlib.Data.Matrix.DualNumber public import Mathlib.Data.Matrix.Invertible public import Mathlib.Data.Matrix.Mul @@ -4148,15 +4203,6 @@ public import Mathlib.Data.Multiset.Sum public import Mathlib.Data.Multiset.Sym public import Mathlib.Data.Multiset.UnionInter public import Mathlib.Data.Multiset.ZeroCons -public import Mathlib.Data.NNRat.BigOperators -public import Mathlib.Data.NNRat.Defs -public import Mathlib.Data.NNRat.Encodable -public import Mathlib.Data.NNRat.Floor -public import Mathlib.Data.NNRat.Lemmas -public import Mathlib.Data.NNRat.Order -public import Mathlib.Data.NNReal.Basic -public import Mathlib.Data.NNReal.Defs -public import Mathlib.Data.NNReal.Star public import Mathlib.Data.Nat.Basic public import Mathlib.Data.Nat.BinaryRec public import Mathlib.Data.Nat.BitIndices @@ -4182,6 +4228,7 @@ public import Mathlib.Data.Nat.Choose.Central public import Mathlib.Data.Nat.Choose.Dvd public import Mathlib.Data.Nat.Choose.Factorization public import Mathlib.Data.Nat.Choose.Lucas +public import Mathlib.Data.Nat.Choose.Mul public import Mathlib.Data.Nat.Choose.Multinomial public import Mathlib.Data.Nat.Choose.Sum public import Mathlib.Data.Nat.Choose.Vandermonde @@ -4223,7 +4270,6 @@ public import Mathlib.Data.Nat.Notation public import Mathlib.Data.Nat.Nth public import Mathlib.Data.Nat.NthRoot.Defs public import Mathlib.Data.Nat.Order.Lemmas -public import Mathlib.Data.Nat.PSub public import Mathlib.Data.Nat.Pairing public import Mathlib.Data.Nat.Periodic public import Mathlib.Data.Nat.Prime.Basic @@ -4234,6 +4280,7 @@ public import Mathlib.Data.Nat.Prime.Int public import Mathlib.Data.Nat.Prime.Nth public import Mathlib.Data.Nat.Prime.Pow public import Mathlib.Data.Nat.PrimeFin +public import Mathlib.Data.Nat.PSub public import Mathlib.Data.Nat.Set public import Mathlib.Data.Nat.Size public import Mathlib.Data.Nat.Sqrt @@ -4242,6 +4289,15 @@ public import Mathlib.Data.Nat.SuccPred public import Mathlib.Data.Nat.Totient public import Mathlib.Data.Nat.Upto public import Mathlib.Data.Nat.WithBot +public import Mathlib.Data.NNRat.BigOperators +public import Mathlib.Data.NNRat.Defs +public import Mathlib.Data.NNRat.Encodable +public import Mathlib.Data.NNRat.Floor +public import Mathlib.Data.NNRat.Lemmas +public import Mathlib.Data.NNRat.Order +public import Mathlib.Data.NNReal.Basic +public import Mathlib.Data.NNReal.Defs +public import Mathlib.Data.NNReal.Star public import Mathlib.Data.Num.Basic public import Mathlib.Data.Num.Bitwise public import Mathlib.Data.Num.Lemmas @@ -4256,6 +4312,7 @@ public import Mathlib.Data.Ordering.Lemmas public import Mathlib.Data.Ordmap.Invariants public import Mathlib.Data.Ordmap.Ordnode public import Mathlib.Data.Ordmap.Ordset +public import Mathlib.Data.Part public import Mathlib.Data.PEquiv public import Mathlib.Data.PFun public import Mathlib.Data.PFunctor.Multivariate.Basic @@ -4263,6 +4320,7 @@ public import Mathlib.Data.PFunctor.Multivariate.M public import Mathlib.Data.PFunctor.Multivariate.W public import Mathlib.Data.PFunctor.Univariate.Basic public import Mathlib.Data.PFunctor.Univariate.M +public import Mathlib.Data.Pi.Interval public import Mathlib.Data.PNat.Basic public import Mathlib.Data.PNat.Defs public import Mathlib.Data.PNat.Equiv @@ -4273,13 +4331,11 @@ public import Mathlib.Data.PNat.Notation public import Mathlib.Data.PNat.Order public import Mathlib.Data.PNat.Prime public import Mathlib.Data.PNat.Xgcd -public import Mathlib.Data.PSigma.Order -public import Mathlib.Data.Part -public import Mathlib.Data.Pi.Interval public import Mathlib.Data.Prod.Basic public import Mathlib.Data.Prod.Lex public import Mathlib.Data.Prod.PProd public import Mathlib.Data.Prod.TProd +public import Mathlib.Data.PSigma.Order public import Mathlib.Data.QPF.Multivariate.Basic public import Mathlib.Data.QPF.Multivariate.Constructions.Cofix public import Mathlib.Data.QPF.Multivariate.Constructions.Comp @@ -4311,8 +4367,8 @@ public import Mathlib.Data.Real.Archimedean public import Mathlib.Data.Real.Basic public import Mathlib.Data.Real.CompleteField public import Mathlib.Data.Real.ConjExponents -public import Mathlib.Data.Real.ENatENNReal public import Mathlib.Data.Real.Embedding +public import Mathlib.Data.Real.ENatENNReal public import Mathlib.Data.Real.Hom public import Mathlib.Data.Real.Pointwise public import Mathlib.Data.Real.Sign @@ -4322,7 +4378,6 @@ public import Mathlib.Data.Real.StarOrdered public import Mathlib.Data.Rel public import Mathlib.Data.Rel.Cover public import Mathlib.Data.Rel.Separated -public import Mathlib.Data.SProd public import Mathlib.Data.Semiquot public import Mathlib.Data.Seq.Basic public import Mathlib.Data.Seq.Computation @@ -4330,8 +4385,8 @@ public import Mathlib.Data.Seq.Defs public import Mathlib.Data.Seq.Parallel public import Mathlib.Data.Set.Accumulate public import Mathlib.Data.Set.Basic -public import Mathlib.Data.Set.BoolIndicator public import Mathlib.Data.Set.BooleanAlgebra +public import Mathlib.Data.Set.BoolIndicator public import Mathlib.Data.Set.Card public import Mathlib.Data.Set.Card.Arithmetic public import Mathlib.Data.Set.CoeSort @@ -4375,9 +4430,9 @@ public import Mathlib.Data.Set.Pointwise.Support public import Mathlib.Data.Set.PowersetCard public import Mathlib.Data.Set.Prod public import Mathlib.Data.Set.Restrict -public import Mathlib.Data.Set.SMulAntidiagonal public import Mathlib.Data.Set.Semiring public import Mathlib.Data.Set.Sigma +public import Mathlib.Data.Set.SMulAntidiagonal public import Mathlib.Data.Set.Subset public import Mathlib.Data.Set.Subsingleton public import Mathlib.Data.Set.Sups @@ -4394,6 +4449,7 @@ public import Mathlib.Data.Sigma.Lex public import Mathlib.Data.Sigma.Order public import Mathlib.Data.Sign.Basic public import Mathlib.Data.Sign.Defs +public import Mathlib.Data.SProd public import Mathlib.Data.Stream.Defs public import Mathlib.Data.Stream.Init public import Mathlib.Data.String.Basic @@ -4511,6 +4567,7 @@ public import Mathlib.FieldTheory.IntermediateField.Adjoin.Defs public import Mathlib.FieldTheory.IntermediateField.Algebraic public import Mathlib.FieldTheory.IntermediateField.Basic public import Mathlib.FieldTheory.IntermediateField.ExtendRight +public import Mathlib.FieldTheory.Isaacs public import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure public import Mathlib.FieldTheory.IsAlgClosed.Basic public import Mathlib.FieldTheory.IsAlgClosed.Classification @@ -4518,7 +4575,6 @@ public import Mathlib.FieldTheory.IsAlgClosed.Spectrum public import Mathlib.FieldTheory.IsPerfectClosure public import Mathlib.FieldTheory.IsRealClosed.Basic public import Mathlib.FieldTheory.IsSepClosed -public import Mathlib.FieldTheory.Isaacs public import Mathlib.FieldTheory.JacobsonNoether public import Mathlib.FieldTheory.KrullTopology public import Mathlib.FieldTheory.KummerExtension @@ -4620,8 +4676,8 @@ public import Mathlib.Geometry.Group.Growth.QuotientInter public import Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation public import Mathlib.Geometry.Manifold.Algebra.LieGroup public import Mathlib.Geometry.Manifold.Algebra.Monoid -public import Mathlib.Geometry.Manifold.Algebra.SMul public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions +public import Mathlib.Geometry.Manifold.Algebra.SMul public import Mathlib.Geometry.Manifold.Algebra.Structures public import Mathlib.Geometry.Manifold.Bordism public import Mathlib.Geometry.Manifold.BumpFunction @@ -4633,8 +4689,8 @@ public import Mathlib.Geometry.Manifold.ContMDiff.Basic public import Mathlib.Geometry.Manifold.ContMDiff.Constructions public import Mathlib.Geometry.Manifold.ContMDiff.Defs public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace -public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv public import Mathlib.Geometry.Manifold.ContMDiffMap +public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv public import Mathlib.Geometry.Manifold.DerivationBundle public import Mathlib.Geometry.Manifold.Diffeomorph public import Mathlib.Geometry.Manifold.GroupLieAlgebra @@ -4655,6 +4711,7 @@ public import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary public import Mathlib.Geometry.Manifold.LocalDiffeomorph public import Mathlib.Geometry.Manifold.LocalInvariantProperties public import Mathlib.Geometry.Manifold.LocalSourceTargetProperty +public import Mathlib.Geometry.Manifold.Metrizable public import Mathlib.Geometry.Manifold.MFDeriv.Atlas public import Mathlib.Geometry.Manifold.MFDeriv.Basic public import Mathlib.Geometry.Manifold.MFDeriv.Defs @@ -4663,7 +4720,6 @@ public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions public import Mathlib.Geometry.Manifold.MFDeriv.Tangent public import Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential -public import Mathlib.Geometry.Manifold.Metrizable public import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.PartitionOfUnity public import Mathlib.Geometry.Manifold.PoincareConjecture @@ -4788,8 +4844,8 @@ public import Mathlib.GroupTheory.GroupExtension.Basic public import Mathlib.GroupTheory.GroupExtension.Defs public import Mathlib.GroupTheory.HNNExtension public import Mathlib.GroupTheory.Index -public import Mathlib.GroupTheory.IndexNSmul public import Mathlib.GroupTheory.IndexNormal +public import Mathlib.GroupTheory.IndexNSmul public import Mathlib.GroupTheory.IsPerfect public import Mathlib.GroupTheory.IsSubnormal public import Mathlib.GroupTheory.MonoidLocalization.Away @@ -4810,7 +4866,6 @@ public import Mathlib.GroupTheory.OrderOfElement public import Mathlib.GroupTheory.OreLocalization.Basic public import Mathlib.GroupTheory.OreLocalization.Cardinality public import Mathlib.GroupTheory.OreLocalization.OreSet -public import Mathlib.GroupTheory.PGroup public import Mathlib.GroupTheory.Perm.Basic public import Mathlib.GroupTheory.Perm.Centralizer public import Mathlib.GroupTheory.Perm.Closure @@ -4831,6 +4886,7 @@ public import Mathlib.GroupTheory.Perm.Sign public import Mathlib.GroupTheory.Perm.Subgroup public import Mathlib.GroupTheory.Perm.Support public import Mathlib.GroupTheory.Perm.ViaEmbedding +public import Mathlib.GroupTheory.PGroup public import Mathlib.GroupTheory.PresentedGroup public import Mathlib.GroupTheory.PushoutI public import Mathlib.GroupTheory.QuotientGroup.Basic @@ -4986,8 +5042,8 @@ public import Mathlib.LinearAlgebra.ConvexSpace public import Mathlib.LinearAlgebra.ConvexSpace.AffineSpace public import Mathlib.LinearAlgebra.Countable public import Mathlib.LinearAlgebra.CrossProduct -public import Mathlib.LinearAlgebra.DFinsupp public import Mathlib.LinearAlgebra.Determinant +public import Mathlib.LinearAlgebra.DFinsupp public import Mathlib.LinearAlgebra.Dimension.Basic public import Mathlib.LinearAlgebra.Dimension.Constructions public import Mathlib.LinearAlgebra.Dimension.DivisionRing @@ -5033,8 +5089,8 @@ public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas public import Mathlib.LinearAlgebra.FiniteSpan public import Mathlib.LinearAlgebra.Finsupp.Defs -public import Mathlib.LinearAlgebra.Finsupp.LSum public import Mathlib.LinearAlgebra.Finsupp.LinearCombination +public import Mathlib.LinearAlgebra.Finsupp.LSum public import Mathlib.LinearAlgebra.Finsupp.Pi public import Mathlib.LinearAlgebra.Finsupp.Span public import Mathlib.LinearAlgebra.Finsupp.SumProd @@ -5055,6 +5111,7 @@ public import Mathlib.LinearAlgebra.FreeModule.Norm public import Mathlib.LinearAlgebra.FreeModule.PID public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition public import Mathlib.LinearAlgebra.FreeProduct.Basic +public import Mathlib.LinearAlgebra.GeneralLinearGroup public import Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv public import Mathlib.LinearAlgebra.GeneralLinearGroup.Basic public import Mathlib.LinearAlgebra.Goursat @@ -5109,6 +5166,7 @@ public import Mathlib.LinearAlgebra.Matrix.Gershgorin public import Mathlib.LinearAlgebra.Matrix.Hadamard public import Mathlib.LinearAlgebra.Matrix.HadamardMatrix public import Mathlib.LinearAlgebra.Matrix.Hermitian +public import Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus public import Mathlib.LinearAlgebra.Matrix.Ideal public import Mathlib.LinearAlgebra.Matrix.Integer public import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber @@ -5116,6 +5174,7 @@ public import Mathlib.LinearAlgebra.Matrix.Invertible public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs public import Mathlib.LinearAlgebra.Matrix.IsDiag public import Mathlib.LinearAlgebra.Matrix.Kronecker +public import Mathlib.LinearAlgebra.Matrix.LDL public import Mathlib.LinearAlgebra.Matrix.Module public import Mathlib.LinearAlgebra.Matrix.MvPolynomial public import Mathlib.LinearAlgebra.Matrix.Nondegenerate @@ -5157,10 +5216,10 @@ public import Mathlib.LinearAlgebra.Multilinear.Finsupp public import Mathlib.LinearAlgebra.Multilinear.Pi public import Mathlib.LinearAlgebra.Multilinear.TensorProduct public import Mathlib.LinearAlgebra.Orientation -public import Mathlib.LinearAlgebra.PID public import Mathlib.LinearAlgebra.PerfectPairing.Basic public import Mathlib.LinearAlgebra.PerfectPairing.Restrict public import Mathlib.LinearAlgebra.Pi +public import Mathlib.LinearAlgebra.PID public import Mathlib.LinearAlgebra.PiTensorProduct public import Mathlib.LinearAlgebra.PiTensorProduct.Basic public import Mathlib.LinearAlgebra.PiTensorProduct.Basis @@ -5228,13 +5287,14 @@ public import Mathlib.LinearAlgebra.RootSystem.Reduced public import Mathlib.LinearAlgebra.RootSystem.RootPairingCat public import Mathlib.LinearAlgebra.RootSystem.RootPositive public import Mathlib.LinearAlgebra.RootSystem.WeylGroup -public import Mathlib.LinearAlgebra.SModEq.Basic -public import Mathlib.LinearAlgebra.SModEq.Pointwise -public import Mathlib.LinearAlgebra.SModEq.Pow public import Mathlib.LinearAlgebra.Semisimple public import Mathlib.LinearAlgebra.SesquilinearForm.Basic public import Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal public import Mathlib.LinearAlgebra.SesquilinearForm.Star +public import Mathlib.LinearAlgebra.SModEq +public import Mathlib.LinearAlgebra.SModEq.Basic +public import Mathlib.LinearAlgebra.SModEq.Pointwise +public import Mathlib.LinearAlgebra.SModEq.Pow public import Mathlib.LinearAlgebra.Span.Basic public import Mathlib.LinearAlgebra.Span.Defs public import Mathlib.LinearAlgebra.Span.TensorProduct @@ -5363,18 +5423,18 @@ public import Mathlib.MeasureTheory.Covering.LiminfLimsup public import Mathlib.MeasureTheory.Covering.OneDim public import Mathlib.MeasureTheory.Covering.Vitali public import Mathlib.MeasureTheory.Covering.VitaliFamily +public import Mathlib.MeasureTheory.Function.AbsolutelyContinuous public import Mathlib.MeasureTheory.Function.AEEqFun public import Mathlib.MeasureTheory.Function.AEEqFun.DomAct public import Mathlib.MeasureTheory.Function.AEEqOfIntegral public import Mathlib.MeasureTheory.Function.AEEqOfLIntegral public import Mathlib.MeasureTheory.Function.AEMeasurableOrder public import Mathlib.MeasureTheory.Function.AEMeasurableSequence -public import Mathlib.MeasureTheory.Function.AbsolutelyContinuous public import Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic -public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 +public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator public import Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner public import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut @@ -5435,11 +5495,11 @@ public import Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal public import Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner public import Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas public import Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp -public import Mathlib.MeasureTheory.Function.UnifTight public import Mathlib.MeasureTheory.Function.UniformIntegrable -public import Mathlib.MeasureTheory.Group.AEStabilizer +public import Mathlib.MeasureTheory.Function.UnifTight public import Mathlib.MeasureTheory.Group.Action public import Mathlib.MeasureTheory.Group.AddCircle +public import Mathlib.MeasureTheory.Group.AEStabilizer public import Mathlib.MeasureTheory.Group.Arithmetic public import Mathlib.MeasureTheory.Group.Convolution public import Mathlib.MeasureTheory.Group.Defs @@ -5527,10 +5587,10 @@ public import Mathlib.MeasureTheory.MeasurableSpace.NCard public import Mathlib.MeasureTheory.MeasurableSpace.Pi public import Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict public import Mathlib.MeasureTheory.MeasurableSpace.Prod -public import Mathlib.MeasureTheory.Measure.AEDisjoint -public import Mathlib.MeasureTheory.Measure.AEMeasurable public import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous public import Mathlib.MeasureTheory.Measure.AddContent +public import Mathlib.MeasureTheory.Measure.AEDisjoint +public import Mathlib.MeasureTheory.Measure.AEMeasurable public import Mathlib.MeasureTheory.Measure.CharacteristicFunction public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion @@ -5576,9 +5636,9 @@ public import Mathlib.MeasureTheory.Measure.LevyConvergence public import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric public import Mathlib.MeasureTheory.Measure.LogLikelihoodRatio public import Mathlib.MeasureTheory.Measure.Map +public import Mathlib.MeasureTheory.Measure.MeasuredSets public import Mathlib.MeasureTheory.Measure.MeasureSpace public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef -public import Mathlib.MeasureTheory.Measure.MeasuredSets public import Mathlib.MeasureTheory.Measure.MutuallySingular public import Mathlib.MeasureTheory.Measure.NullMeasurable public import Mathlib.MeasureTheory.Measure.OpenPos @@ -5679,9 +5739,10 @@ public import Mathlib.ModelTheory.Syntax public import Mathlib.ModelTheory.Topology.Types public import Mathlib.ModelTheory.Types public import Mathlib.ModelTheory.Ultraproducts -public import Mathlib.NumberTheory.ADEInequality public import Mathlib.NumberTheory.AbelSummation +public import Mathlib.NumberTheory.ADEInequality public import Mathlib.NumberTheory.AlmostPrime +public import Mathlib.NumberTheory.ArithmeticFunction public import Mathlib.NumberTheory.ArithmeticFunction.Carmichael public import Mathlib.NumberTheory.ArithmeticFunction.Defs public import Mathlib.NumberTheory.ArithmeticFunction.LFunction @@ -5717,14 +5778,14 @@ public import Mathlib.NumberTheory.EllipticDivisibilitySequence public import Mathlib.NumberTheory.EulerProduct.Basic public import Mathlib.NumberTheory.EulerProduct.DirichletLSeries public import Mathlib.NumberTheory.EulerProduct.ExpLog +public import Mathlib.NumberTheory.FactorisationProperties +public import Mathlib.NumberTheory.Fermat +public import Mathlib.NumberTheory.FermatPsp public import Mathlib.NumberTheory.FLT.Basic public import Mathlib.NumberTheory.FLT.Four public import Mathlib.NumberTheory.FLT.MasonStothers public import Mathlib.NumberTheory.FLT.Polynomial public import Mathlib.NumberTheory.FLT.Three -public import Mathlib.NumberTheory.FactorisationProperties -public import Mathlib.NumberTheory.Fermat -public import Mathlib.NumberTheory.FermatPsp public import Mathlib.NumberTheory.FrobeniusNumber public import Mathlib.NumberTheory.FunctionField public import Mathlib.NumberTheory.GaussSum @@ -5742,6 +5803,16 @@ public import Mathlib.NumberTheory.Height.NumberField public import Mathlib.NumberTheory.Height.Projectivization public import Mathlib.NumberTheory.JacobiSum.Basic public import Mathlib.NumberTheory.KummerDedekind +public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter +public import Mathlib.NumberTheory.LegendreSymbol.Basic +public import Mathlib.NumberTheory.LegendreSymbol.Complex +public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas +public import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol +public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic +public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum +public import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity +public import Mathlib.NumberTheory.LegendreSymbol.ZModChar +public import Mathlib.NumberTheory.LocalField.Basic public import Mathlib.NumberTheory.LSeries.AbstractFuncEq public import Mathlib.NumberTheory.LSeries.Basic public import Mathlib.NumberTheory.LSeries.Convergence @@ -5761,18 +5832,8 @@ public import Mathlib.NumberTheory.LSeries.Positivity public import Mathlib.NumberTheory.LSeries.PrimesInAP public import Mathlib.NumberTheory.LSeries.RiemannZeta public import Mathlib.NumberTheory.LSeries.SumCoeff -public import Mathlib.NumberTheory.LSeries.ZMod public import Mathlib.NumberTheory.LSeries.ZetaZeros -public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter -public import Mathlib.NumberTheory.LegendreSymbol.Basic -public import Mathlib.NumberTheory.LegendreSymbol.Complex -public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas -public import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol -public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic -public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum -public import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity -public import Mathlib.NumberTheory.LegendreSymbol.ZModChar -public import Mathlib.NumberTheory.LocalField.Basic +public import Mathlib.NumberTheory.LSeries.ZMod public import Mathlib.NumberTheory.LucasLehmer public import Mathlib.NumberTheory.LucasPrimality public import Mathlib.NumberTheory.MahlerMeasure @@ -5823,13 +5884,13 @@ public import Mathlib.NumberTheory.Multiplicity public import Mathlib.NumberTheory.Niven public import Mathlib.NumberTheory.NumberField.AdeleRing public import Mathlib.NumberTheory.NumberField.Basic -public import Mathlib.NumberTheory.NumberField.CMField public import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic public import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody public import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone public import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne public import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord public import Mathlib.NumberTheory.NumberField.ClassNumber +public import Mathlib.NumberTheory.NumberField.CMField public import Mathlib.NumberTheory.NumberField.Completion.FinitePlace public import Mathlib.NumberTheory.NumberField.Completion.InfinitePlace public import Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances @@ -5909,6 +5970,8 @@ public import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith public import Mathlib.NumberTheory.Transcendental.Liouville.Measure public import Mathlib.NumberTheory.Transcendental.Liouville.Residual public import Mathlib.NumberTheory.TsumDivisorsAntidiagonal +public import Mathlib.NumberTheory.TsumDivsorsAntidiagonal +public import Mathlib.NumberTheory.VonMangoldt public import Mathlib.NumberTheory.WellApproximable public import Mathlib.NumberTheory.Wilson public import Mathlib.NumberTheory.ZetaValues @@ -5926,8 +5989,8 @@ public import Mathlib.Order.BooleanAlgebra.Basic public import Mathlib.Order.BooleanAlgebra.Defs public import Mathlib.Order.BooleanAlgebra.Set public import Mathlib.Order.BooleanGenerators -public import Mathlib.Order.BooleanSubalgebra public import Mathlib.Order.Booleanisation +public import Mathlib.Order.BooleanSubalgebra public import Mathlib.Order.Bounded public import Mathlib.Order.BoundedOrder.Basic public import Mathlib.Order.BoundedOrder.Lattice @@ -5996,9 +6059,9 @@ public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Defs.Prop public import Mathlib.Order.Defs.Unbundled -public import Mathlib.Order.DirSupClosed public import Mathlib.Order.Directed public import Mathlib.Order.DirectedInverseSystem +public import Mathlib.Order.DirSupClosed public import Mathlib.Order.Disjoint public import Mathlib.Order.Disjointed public import Mathlib.Order.Extension.Linear @@ -6137,8 +6200,8 @@ public import Mathlib.Order.LatticeIntervals public import Mathlib.Order.Lex public import Mathlib.Order.LiminfLimsup public import Mathlib.Order.Max -public import Mathlib.Order.MinMax public import Mathlib.Order.Minimal +public import Mathlib.Order.MinMax public import Mathlib.Order.ModularLattice public import Mathlib.Order.Monotone.Basic public import Mathlib.Order.Monotone.Defs @@ -6156,12 +6219,12 @@ public import Mathlib.Order.OmegaCompletePartialOrder public import Mathlib.Order.OrdContinuous public import Mathlib.Order.OrderDual public import Mathlib.Order.OrderIsoNat -public import Mathlib.Order.PFilter public import Mathlib.Order.Part public import Mathlib.Order.PartialSups public import Mathlib.Order.Partition.Basic public import Mathlib.Order.Partition.Equipartition public import Mathlib.Order.Partition.Finpartition +public import Mathlib.Order.PFilter public import Mathlib.Order.PiLex public import Mathlib.Order.Preorder.Chain public import Mathlib.Order.Preorder.Finite @@ -6208,9 +6271,9 @@ public import Mathlib.Order.SymmDiff public import Mathlib.Order.Synonym public import Mathlib.Order.TeichmullerTukey public import Mathlib.Order.TransfiniteIteration -public import Mathlib.Order.TypeTags public import Mathlib.Order.Types.Arithmetic public import Mathlib.Order.Types.Defs +public import Mathlib.Order.TypeTags public import Mathlib.Order.ULift public import Mathlib.Order.UpperLower.Basic public import Mathlib.Order.UpperLower.Closure @@ -6234,9 +6297,9 @@ public import Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily public import Mathlib.Probability.CDF public import Mathlib.Probability.CentralLimitTheorem public import Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs -public import Mathlib.Probability.CondVar public import Mathlib.Probability.ConditionalExpectation public import Mathlib.Probability.ConditionalProbability +public import Mathlib.Probability.CondVar public import Mathlib.Probability.Decision.BayesEstimator public import Mathlib.Probability.Decision.Risk.Basic public import Mathlib.Probability.Decision.Risk.Countable @@ -6279,6 +6342,7 @@ public import Mathlib.Probability.Independence.Conditional public import Mathlib.Probability.Independence.InfinitePi public import Mathlib.Probability.Independence.Integrable public import Mathlib.Probability.Independence.Integration +public import Mathlib.Probability.Independence.Kernel public import Mathlib.Probability.Independence.Kernel.Indep public import Mathlib.Probability.Independence.Kernel.IndepFun public import Mathlib.Probability.Independence.Process.Basic @@ -6289,7 +6353,6 @@ public import Mathlib.Probability.Independence.ZeroOne public import Mathlib.Probability.Kernel.Basic public import Mathlib.Probability.Kernel.Category.SFinKer public import Mathlib.Probability.Kernel.Category.Stoch -public import Mathlib.Probability.Kernel.CompProdEqIff public import Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous public import Mathlib.Probability.Kernel.Composition.Comp public import Mathlib.Probability.Kernel.Composition.CompMap @@ -6304,6 +6367,7 @@ public import Mathlib.Probability.Kernel.Composition.MeasureCompProd public import Mathlib.Probability.Kernel.Composition.ParallelComp public import Mathlib.Probability.Kernel.Composition.Prod public import Mathlib.Probability.Kernel.Composition.RadonNikodym +public import Mathlib.Probability.Kernel.CompProdEqIff public import Mathlib.Probability.Kernel.CondDistrib public import Mathlib.Probability.Kernel.Condexp public import Mathlib.Probability.Kernel.Defs @@ -6427,7 +6491,6 @@ public import Mathlib.RingTheory.Adjoin.PowerBasis public import Mathlib.RingTheory.Adjoin.Singleton public import Mathlib.RingTheory.Adjoin.Tower public import Mathlib.RingTheory.AdjoinRoot -public import Mathlib.RingTheory.AlgebraTower public import Mathlib.RingTheory.Algebraic.Basic public import Mathlib.RingTheory.Algebraic.Cardinality public import Mathlib.RingTheory.Algebraic.Defs @@ -6443,6 +6506,7 @@ public import Mathlib.RingTheory.AlgebraicIndependent.Defs public import Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis public import Mathlib.RingTheory.AlgebraicIndependent.Transcendental +public import Mathlib.RingTheory.AlgebraTower public import Mathlib.RingTheory.Artinian.Algebra public import Mathlib.RingTheory.Artinian.Defs public import Mathlib.RingTheory.Artinian.Instances @@ -6497,8 +6561,8 @@ public import Mathlib.RingTheory.DedekindDomain.Instances public import Mathlib.RingTheory.DedekindDomain.IntegralClosure public import Mathlib.RingTheory.DedekindDomain.LinearDisjoint public import Mathlib.RingTheory.DedekindDomain.PID -public import Mathlib.RingTheory.DedekindDomain.SInteger public import Mathlib.RingTheory.DedekindDomain.SelmerGroup +public import Mathlib.RingTheory.DedekindDomain.SInteger public import Mathlib.RingTheory.Derivation.Basic public import Mathlib.RingTheory.Derivation.DifferentialRing public import Mathlib.RingTheory.Derivation.Lie @@ -6540,9 +6604,6 @@ public import Mathlib.RingTheory.Extension.Presentation.Submersive public import Mathlib.RingTheory.FilteredAlgebra.Basic public import Mathlib.RingTheory.Filtration public import Mathlib.RingTheory.FiniteLength -public import Mathlib.RingTheory.FinitePresentation -public import Mathlib.RingTheory.FiniteStability -public import Mathlib.RingTheory.FiniteType public import Mathlib.RingTheory.Finiteness.Basic public import Mathlib.RingTheory.Finiteness.Bilinear public import Mathlib.RingTheory.Finiteness.Cardinality @@ -6563,6 +6624,9 @@ public import Mathlib.RingTheory.Finiteness.Projective public import Mathlib.RingTheory.Finiteness.Quotient public import Mathlib.RingTheory.Finiteness.Small public import Mathlib.RingTheory.Finiteness.Subalgebra +public import Mathlib.RingTheory.FinitePresentation +public import Mathlib.RingTheory.FiniteStability +public import Mathlib.RingTheory.FiniteType public import Mathlib.RingTheory.Fintype public import Mathlib.RingTheory.Flat.Basic public import Mathlib.RingTheory.Flat.CategoryTheory @@ -6604,8 +6668,8 @@ public import Mathlib.RingTheory.HahnSeries.Addition public import Mathlib.RingTheory.HahnSeries.Basic public import Mathlib.RingTheory.HahnSeries.Binomial public import Mathlib.RingTheory.HahnSeries.Cardinal -public import Mathlib.RingTheory.HahnSeries.HEval public import Mathlib.RingTheory.HahnSeries.HahnEmbedding +public import Mathlib.RingTheory.HahnSeries.HEval public import Mathlib.RingTheory.HahnSeries.Lex public import Mathlib.RingTheory.HahnSeries.Multiplication public import Mathlib.RingTheory.HahnSeries.PowerSeries @@ -6678,8 +6742,8 @@ public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic public import Mathlib.RingTheory.IntegralClosure.Algebra.Defs public import Mathlib.RingTheory.IntegralClosure.Algebra.Ideal public import Mathlib.RingTheory.IntegralClosure.GoingDown -public import Mathlib.RingTheory.IntegralClosure.IntegralRestrict public import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed +public import Mathlib.RingTheory.IntegralClosure.IntegralRestrict public import Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs @@ -6720,6 +6784,31 @@ public import Mathlib.RingTheory.Length public import Mathlib.RingTheory.LinearDisjoint public import Mathlib.RingTheory.LittleWedderburn public import Mathlib.RingTheory.LocalIso +public import Mathlib.RingTheory.Localization.Algebra +public import Mathlib.RingTheory.Localization.AsSubring +public import Mathlib.RingTheory.Localization.AtPrime.Basic +public import Mathlib.RingTheory.Localization.AtPrime.Extension +public import Mathlib.RingTheory.Localization.Away.AdjoinRoot +public import Mathlib.RingTheory.Localization.Away.Basic +public import Mathlib.RingTheory.Localization.Away.Lemmas +public import Mathlib.RingTheory.Localization.BaseChange +public import Mathlib.RingTheory.Localization.Basic +public import Mathlib.RingTheory.Localization.Cardinality +public import Mathlib.RingTheory.Localization.Defs +public import Mathlib.RingTheory.Localization.Finiteness +public import Mathlib.RingTheory.Localization.FractionRing +public import Mathlib.RingTheory.Localization.Free +public import Mathlib.RingTheory.Localization.Ideal +public import Mathlib.RingTheory.Localization.Integer +public import Mathlib.RingTheory.Localization.Integral +public import Mathlib.RingTheory.Localization.InvSubmonoid +public import Mathlib.RingTheory.Localization.LocalizationLocalization +public import Mathlib.RingTheory.Localization.Module +public import Mathlib.RingTheory.Localization.NormTrace +public import Mathlib.RingTheory.Localization.NumDen +public import Mathlib.RingTheory.Localization.Pi +public import Mathlib.RingTheory.Localization.Rat +public import Mathlib.RingTheory.Localization.Submodule public import Mathlib.RingTheory.LocalProperties.Basic public import Mathlib.RingTheory.LocalProperties.Exactness public import Mathlib.RingTheory.LocalProperties.FinitePresentation @@ -6751,31 +6840,6 @@ public import Mathlib.RingTheory.LocalRing.ResidueField.Instances public import Mathlib.RingTheory.LocalRing.ResidueField.Polynomial public import Mathlib.RingTheory.LocalRing.RingHom.Basic public import Mathlib.RingTheory.LocalRing.Subring -public import Mathlib.RingTheory.Localization.Algebra -public import Mathlib.RingTheory.Localization.AsSubring -public import Mathlib.RingTheory.Localization.AtPrime.Basic -public import Mathlib.RingTheory.Localization.AtPrime.Extension -public import Mathlib.RingTheory.Localization.Away.AdjoinRoot -public import Mathlib.RingTheory.Localization.Away.Basic -public import Mathlib.RingTheory.Localization.Away.Lemmas -public import Mathlib.RingTheory.Localization.BaseChange -public import Mathlib.RingTheory.Localization.Basic -public import Mathlib.RingTheory.Localization.Cardinality -public import Mathlib.RingTheory.Localization.Defs -public import Mathlib.RingTheory.Localization.Finiteness -public import Mathlib.RingTheory.Localization.FractionRing -public import Mathlib.RingTheory.Localization.Free -public import Mathlib.RingTheory.Localization.Ideal -public import Mathlib.RingTheory.Localization.Integer -public import Mathlib.RingTheory.Localization.Integral -public import Mathlib.RingTheory.Localization.InvSubmonoid -public import Mathlib.RingTheory.Localization.LocalizationLocalization -public import Mathlib.RingTheory.Localization.Module -public import Mathlib.RingTheory.Localization.NormTrace -public import Mathlib.RingTheory.Localization.NumDen -public import Mathlib.RingTheory.Localization.Pi -public import Mathlib.RingTheory.Localization.Rat -public import Mathlib.RingTheory.Localization.Submodule public import Mathlib.RingTheory.MatrixAlgebra public import Mathlib.RingTheory.MatrixPolynomialAlgebra public import Mathlib.RingTheory.Morita.Basic @@ -6819,7 +6883,6 @@ public import Mathlib.RingTheory.Nilpotent.Defs public import Mathlib.RingTheory.Nilpotent.Exp public import Mathlib.RingTheory.Nilpotent.GeometricallyReduced public import Mathlib.RingTheory.Nilpotent.Lemmas -public import Mathlib.RingTheory.NoetherNormalization public import Mathlib.RingTheory.Noetherian.Basic public import Mathlib.RingTheory.Noetherian.Defs public import Mathlib.RingTheory.Noetherian.Filter @@ -6827,6 +6890,7 @@ public import Mathlib.RingTheory.Noetherian.Nilpotent public import Mathlib.RingTheory.Noetherian.OfPrime public import Mathlib.RingTheory.Noetherian.Orzech public import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain +public import Mathlib.RingTheory.NoetherNormalization public import Mathlib.RingTheory.NonUnitalSubring.Basic public import Mathlib.RingTheory.NonUnitalSubring.Defs public import Mathlib.RingTheory.NonUnitalSubsemiring.Basic @@ -6834,8 +6898,8 @@ public import Mathlib.RingTheory.NonUnitalSubsemiring.Defs public import Mathlib.RingTheory.Norm.Basic public import Mathlib.RingTheory.Norm.Defs public import Mathlib.RingTheory.Norm.Transitivity -public import Mathlib.RingTheory.NormTrace public import Mathlib.RingTheory.NormalClosure +public import Mathlib.RingTheory.NormTrace public import Mathlib.RingTheory.Nullstellensatz public import Mathlib.RingTheory.OrderOfVanishing.Basic public import Mathlib.RingTheory.OrderOfVanishing.Noetherian @@ -6849,8 +6913,8 @@ public import Mathlib.RingTheory.Perfection public import Mathlib.RingTheory.Perfectoid.BDeRham public import Mathlib.RingTheory.Perfectoid.FontaineTheta public import Mathlib.RingTheory.Perfectoid.Untilt -public import Mathlib.RingTheory.PiTensorProduct public import Mathlib.RingTheory.PicardGroup +public import Mathlib.RingTheory.PiTensorProduct public import Mathlib.RingTheory.Polynomial.Basic public import Mathlib.RingTheory.Polynomial.Bernstein public import Mathlib.RingTheory.Polynomial.Chebyshev @@ -7102,8 +7166,8 @@ public import Mathlib.RingTheory.WittVector.Frobenius public import Mathlib.RingTheory.WittVector.FrobeniusFractionField public import Mathlib.RingTheory.WittVector.Identities public import Mathlib.RingTheory.WittVector.InitTail -public import Mathlib.RingTheory.WittVector.IsPoly public import Mathlib.RingTheory.WittVector.Isocrystal +public import Mathlib.RingTheory.WittVector.IsPoly public import Mathlib.RingTheory.WittVector.MulCoeff public import Mathlib.RingTheory.WittVector.MulP public import Mathlib.RingTheory.WittVector.StructurePolynomial @@ -7112,10 +7176,10 @@ public import Mathlib.RingTheory.WittVector.TeichmullerSeries public import Mathlib.RingTheory.WittVector.Truncated public import Mathlib.RingTheory.WittVector.Verschiebung public import Mathlib.RingTheory.WittVector.WittPolynomial +public import Mathlib.RingTheory.ZariskisMainTheorem public import Mathlib.RingTheory.ZMod public import Mathlib.RingTheory.ZMod.Torsion public import Mathlib.RingTheory.ZMod.UnitsCyclic -public import Mathlib.RingTheory.ZariskisMainTheorem public import Mathlib.SetTheory.Cardinal.Aleph public import Mathlib.SetTheory.Cardinal.Arithmetic public import Mathlib.SetTheory.Cardinal.Basic @@ -7128,8 +7192,8 @@ public import Mathlib.SetTheory.Cardinal.Continuum public import Mathlib.SetTheory.Cardinal.CountableCover public import Mathlib.SetTheory.Cardinal.Defs public import Mathlib.SetTheory.Cardinal.Divisibility -public import Mathlib.SetTheory.Cardinal.ENat public import Mathlib.SetTheory.Cardinal.Embedding +public import Mathlib.SetTheory.Cardinal.ENat public import Mathlib.SetTheory.Cardinal.EventuallyConst public import Mathlib.SetTheory.Cardinal.Finite public import Mathlib.SetTheory.Cardinal.Finsupp @@ -7186,8 +7250,8 @@ public import Mathlib.Tactic.ArithMult public import Mathlib.Tactic.ArithMult.Init public import Mathlib.Tactic.Attr.Core public import Mathlib.Tactic.Attr.Register -public import Mathlib.Tactic.BDSimp public import Mathlib.Tactic.Basic +public import Mathlib.Tactic.BDSimp public import Mathlib.Tactic.Bound public import Mathlib.Tactic.Bound.Attribute public import Mathlib.Tactic.Bound.Init @@ -7225,9 +7289,9 @@ public import Mathlib.Tactic.Change public import Mathlib.Tactic.Check public import Mathlib.Tactic.Choose public import Mathlib.Tactic.Clean +public import Mathlib.Tactic.Clear_ public import Mathlib.Tactic.ClearExcept public import Mathlib.Tactic.ClearExclamation -public import Mathlib.Tactic.Clear_ public import Mathlib.Tactic.ClickSuggestions public import Mathlib.Tactic.ClickSuggestions.Apply public import Mathlib.Tactic.ClickSuggestions.ApplyAt @@ -7261,16 +7325,16 @@ public import Mathlib.Tactic.Conv public import Mathlib.Tactic.Convert public import Mathlib.Tactic.Core public import Mathlib.Tactic.CrossRefAttribute -public import Mathlib.Tactic.DSimpPercent public import Mathlib.Tactic.DeclarationNames public import Mathlib.Tactic.DefEqAbuse public import Mathlib.Tactic.DefEqTransformations -public import Mathlib.Tactic.DepRewrite public import Mathlib.Tactic.DeprecateTo +public import Mathlib.Tactic.DepRewrite public import Mathlib.Tactic.DeriveCountable public import Mathlib.Tactic.DeriveEncodable public import Mathlib.Tactic.DeriveFintype public import Mathlib.Tactic.DeriveTraversable +public import Mathlib.Tactic.DSimpPercent public import Mathlib.Tactic.ENatToNat public import Mathlib.Tactic.Eqns public import Mathlib.Tactic.ErwQuestion @@ -7282,9 +7346,9 @@ public import Mathlib.Tactic.Explode.Pretty public import Mathlib.Tactic.Ext public import Mathlib.Tactic.ExtendDoc public import Mathlib.Tactic.ExtractGoal -public import Mathlib.Tactic.FBinop public import Mathlib.Tactic.FailIfNoProgress public import Mathlib.Tactic.FastInstance +public import Mathlib.Tactic.FBinop public import Mathlib.Tactic.Field public import Mathlib.Tactic.FieldSimp public import Mathlib.Tactic.FieldSimp.Attr @@ -7309,10 +7373,11 @@ public import Mathlib.Tactic.GCongr public import Mathlib.Tactic.GCongr.Core public import Mathlib.Tactic.GCongr.CoreAttrs public import Mathlib.Tactic.GCongr.ForwardAttr +public import Mathlib.Tactic.Generalize +public import Mathlib.Tactic.GeneralizeProofs public import Mathlib.Tactic.GRewrite public import Mathlib.Tactic.GRewrite.Core public import Mathlib.Tactic.GRewrite.Elab -public import Mathlib.Tactic.Generalize public import Mathlib.Tactic.GrindAttrs public import Mathlib.Tactic.Group public import Mathlib.Tactic.GuardGoalNums @@ -7321,11 +7386,11 @@ public import Mathlib.Tactic.Have public import Mathlib.Tactic.HaveI public import Mathlib.Tactic.HigherOrder public import Mathlib.Tactic.Hint -public import Mathlib.Tactic.ITauto public import Mathlib.Tactic.InferParam public import Mathlib.Tactic.Inhabit public import Mathlib.Tactic.IntervalCases public import Mathlib.Tactic.IrreducibleDef +public import Mathlib.Tactic.ITauto public import Mathlib.Tactic.Lemma public import Mathlib.Tactic.Lift public import Mathlib.Tactic.Linarith @@ -7428,9 +7493,8 @@ public import Mathlib.Tactic.Order.Graph.Basic public import Mathlib.Tactic.Order.Graph.Tarjan public import Mathlib.Tactic.Order.Preprocessing public import Mathlib.Tactic.Order.ToInt -public import Mathlib.Tactic.PNatToNat -public import Mathlib.Tactic.PPWithUniv public import Mathlib.Tactic.Peel +public import Mathlib.Tactic.PNatToNat public import Mathlib.Tactic.Polynomial.Basic public import Mathlib.Tactic.Polynomial.Core public import Mathlib.Tactic.Polyrith @@ -7438,12 +7502,13 @@ public import Mathlib.Tactic.Positivity public import Mathlib.Tactic.Positivity.Basic public import Mathlib.Tactic.Positivity.Core public import Mathlib.Tactic.Positivity.Finset +public import Mathlib.Tactic.PPWithUniv public import Mathlib.Tactic.ProdAssoc +public import Mathlib.Tactic.Propose public import Mathlib.Tactic.ProxyType public import Mathlib.Tactic.Push public import Mathlib.Tactic.Push.Attr public import Mathlib.Tactic.Qify -public import Mathlib.Tactic.RSuffices public import Mathlib.Tactic.Recall public import Mathlib.Tactic.Recover public import Mathlib.Tactic.ReduceModChar @@ -7463,6 +7528,7 @@ public import Mathlib.Tactic.Ring.NamePolyVars public import Mathlib.Tactic.Ring.NamePowerVars public import Mathlib.Tactic.Ring.PNat public import Mathlib.Tactic.Ring.RingNF +public import Mathlib.Tactic.RSuffices public import Mathlib.Tactic.Sat.FromLRAT public import Mathlib.Tactic.Says public import Mathlib.Tactic.ScopedNS @@ -7470,12 +7536,12 @@ public import Mathlib.Tactic.Set public import Mathlib.Tactic.SetLike public import Mathlib.Tactic.SetNotationForOrder public import Mathlib.Tactic.SimpIntro -public import Mathlib.Tactic.SimpRw public import Mathlib.Tactic.Simproc.Divisors public import Mathlib.Tactic.Simproc.ExistsAndEq public import Mathlib.Tactic.Simproc.Factors public import Mathlib.Tactic.Simproc.FinsetInterval public import Mathlib.Tactic.Simproc.VecPerm +public import Mathlib.Tactic.SimpRw public import Mathlib.Tactic.Simps.Basic public import Mathlib.Tactic.Simps.NotationClass public import Mathlib.Tactic.SplitIfs @@ -7487,12 +7553,12 @@ public import Mathlib.Tactic.SuccessIfFailWithMsg public import Mathlib.Tactic.SudoSetOption public import Mathlib.Tactic.SuppressCompilation public import Mathlib.Tactic.SwapVar -public import Mathlib.Tactic.TFAE public import Mathlib.Tactic.TacticAnalysis public import Mathlib.Tactic.TacticAnalysis.Declarations public import Mathlib.Tactic.Tauto public import Mathlib.Tactic.TautoSet public import Mathlib.Tactic.TermCongr +public import Mathlib.Tactic.TFAE public import Mathlib.Tactic.ToAdditive public import Mathlib.Tactic.ToDual public import Mathlib.Tactic.ToExpr @@ -7513,17 +7579,18 @@ public import Mathlib.Tactic.TypeStar public import Mathlib.Tactic.UnsetOption public import Mathlib.Tactic.Use public import Mathlib.Tactic.Variable -public import Mathlib.Tactic.WLOG public import Mathlib.Tactic.Widget.Calc public import Mathlib.Tactic.Widget.CommDiag public import Mathlib.Tactic.Widget.CongrM public import Mathlib.Tactic.Widget.Conv public import Mathlib.Tactic.Widget.GCongr +public import Mathlib.Tactic.Widget.InteractiveUnfold public import Mathlib.Tactic.Widget.LibraryRewrite public import Mathlib.Tactic.Widget.SelectInsertParamsClass public import Mathlib.Tactic.Widget.SelectPanelUtils public import Mathlib.Tactic.Widget.StringDiagram public import Mathlib.Tactic.WithoutCDot +public import Mathlib.Tactic.WLOG public import Mathlib.Tactic.Zify public import Mathlib.Testing.Plausible.Functions public import Mathlib.Testing.Plausible.Sampleable @@ -7645,13 +7712,13 @@ public import Mathlib.Topology.Algebra.Monoid.Defs public import Mathlib.Topology.Algebra.Monoid.FunOnFinite public import Mathlib.Topology.Algebra.MulAction public import Mathlib.Topology.Algebra.MvPolynomial -public import Mathlib.Topology.Algebra.NonUnitalAlgebra -public import Mathlib.Topology.Algebra.NonUnitalStarAlgebra public import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology public import Mathlib.Topology.Algebra.Nonarchimedean.Bases public import Mathlib.Topology.Algebra.Nonarchimedean.Basic public import Mathlib.Topology.Algebra.Nonarchimedean.Completion public import Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected +public import Mathlib.Topology.Algebra.NonUnitalAlgebra +public import Mathlib.Topology.Algebra.NonUnitalStarAlgebra public import Mathlib.Topology.Algebra.OpenSubgroup public import Mathlib.Topology.Algebra.Order.Archimedean public import Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete @@ -7716,12 +7783,9 @@ public import Mathlib.Topology.Bornology.BoundedOperation public import Mathlib.Topology.Bornology.Constructions public import Mathlib.Topology.Bornology.Hom public import Mathlib.Topology.Bornology.Real -public import Mathlib.Topology.CWComplex.Abstract.Basic -public import Mathlib.Topology.CWComplex.Classical.Basic -public import Mathlib.Topology.CWComplex.Classical.Finite -public import Mathlib.Topology.CWComplex.Classical.Graph -public import Mathlib.Topology.CWComplex.Classical.Subcomplex public import Mathlib.Topology.Category.Born +public import Mathlib.Topology.Category.CompactlyGenerated +public import Mathlib.Topology.Category.Compactum public import Mathlib.Topology.Category.CompHaus.Basic public import Mathlib.Topology.Category.CompHaus.EffectiveEpi public import Mathlib.Topology.Category.CompHaus.Frm @@ -7732,8 +7796,6 @@ public import Mathlib.Topology.Category.CompHausLike.Cartesian public import Mathlib.Topology.Category.CompHausLike.EffectiveEpi public import Mathlib.Topology.Category.CompHausLike.Limits public import Mathlib.Topology.Category.CompHausLike.SigmaComparison -public import Mathlib.Topology.Category.CompactlyGenerated -public import Mathlib.Topology.Category.Compactum public import Mathlib.Topology.Category.DeltaGenerated public import Mathlib.Topology.Category.FinTopCat public import Mathlib.Topology.Category.LightProfinite.AsLimit @@ -7787,30 +7849,32 @@ public import Mathlib.Topology.ClopenBox public import Mathlib.Topology.Closure public import Mathlib.Topology.ClusterPt public import Mathlib.Topology.Coherent -public import Mathlib.Topology.CompactOpen public import Mathlib.Topology.Compactification.OnePoint.Basic public import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine public import Mathlib.Topology.Compactification.OnePoint.Sphere public import Mathlib.Topology.Compactification.StoneCech public import Mathlib.Topology.Compactness.Bases public import Mathlib.Topology.Compactness.Compact -public import Mathlib.Topology.Compactness.CompactSystem public import Mathlib.Topology.Compactness.CompactlyCoherentSpace public import Mathlib.Topology.Compactness.CompactlyGeneratedSpace +public import Mathlib.Topology.Compactness.CompactSystem public import Mathlib.Topology.Compactness.CountablyCompact public import Mathlib.Topology.Compactness.DeltaGeneratedSpace +public import Mathlib.Topology.Compactness.HilbertCubeEmbedding public import Mathlib.Topology.Compactness.Lindelof public import Mathlib.Topology.Compactness.LocallyCompact public import Mathlib.Topology.Compactness.LocallyFinite public import Mathlib.Topology.Compactness.NhdsKer public import Mathlib.Topology.Compactness.Paracompact +public import Mathlib.Topology.Compactness.PseudometrizableLindelof public import Mathlib.Topology.Compactness.SigmaCompact +public import Mathlib.Topology.CompactOpen public import Mathlib.Topology.Connected.Basic public import Mathlib.Topology.Connected.CardComponents public import Mathlib.Topology.Connected.Clopen -public import Mathlib.Topology.Connected.LocPathConnected public import Mathlib.Topology.Connected.LocallyConnected public import Mathlib.Topology.Connected.LocallyPathConnected +public import Mathlib.Topology.Connected.LocPathConnected public import Mathlib.Topology.Connected.PathComponentOne public import Mathlib.Topology.Connected.PathConnected public import Mathlib.Topology.Connected.Separation @@ -7856,9 +7920,15 @@ public import Mathlib.Topology.Convenient.GeneratedBy public import Mathlib.Topology.Convenient.HomSpace public import Mathlib.Topology.Convenient.Localization public import Mathlib.Topology.Convenient.OpenClosed +public import Mathlib.Topology.Covering public import Mathlib.Topology.Covering.AddCircle public import Mathlib.Topology.Covering.Basic public import Mathlib.Topology.Covering.Quotient +public import Mathlib.Topology.CWComplex.Abstract.Basic +public import Mathlib.Topology.CWComplex.Classical.Basic +public import Mathlib.Topology.CWComplex.Classical.Finite +public import Mathlib.Topology.CWComplex.Classical.Graph +public import Mathlib.Topology.CWComplex.Classical.Subcomplex public import Mathlib.Topology.Defs.Basic public import Mathlib.Topology.Defs.Filter public import Mathlib.Topology.Defs.Induced @@ -7900,8 +7970,8 @@ public import Mathlib.Topology.Homotopy.Affine public import Mathlib.Topology.Homotopy.Basic public import Mathlib.Topology.Homotopy.Contractible public import Mathlib.Topology.Homotopy.Equiv -public import Mathlib.Topology.Homotopy.HSpaces public import Mathlib.Topology.Homotopy.HomotopyGroup +public import Mathlib.Topology.Homotopy.HSpaces public import Mathlib.Topology.Homotopy.Lifting public import Mathlib.Topology.Homotopy.LocallyContractible public import Mathlib.Topology.Homotopy.Path @@ -7918,15 +7988,15 @@ public import Mathlib.Topology.Instances.AddCircle.Real public import Mathlib.Topology.Instances.CantorSet public import Mathlib.Topology.Instances.Complex public import Mathlib.Topology.Instances.Discrete +public import Mathlib.Topology.Instances.ENat public import Mathlib.Topology.Instances.ENNReal.ENatENNReal public import Mathlib.Topology.Instances.ENNReal.Lemmas -public import Mathlib.Topology.Instances.ENat public import Mathlib.Topology.Instances.EReal.Lemmas public import Mathlib.Topology.Instances.Int public import Mathlib.Topology.Instances.Irrational public import Mathlib.Topology.Instances.Matrix -public import Mathlib.Topology.Instances.NNReal.Lemmas public import Mathlib.Topology.Instances.Nat +public import Mathlib.Topology.Instances.NNReal.Lemmas public import Mathlib.Topology.Instances.PNat public import Mathlib.Topology.Instances.Rat public import Mathlib.Topology.Instances.RatLemmas @@ -7963,8 +8033,8 @@ public import Mathlib.Topology.MetricSpace.Bilipschitz public import Mathlib.Topology.MetricSpace.Bounded public import Mathlib.Topology.MetricSpace.BundledFun public import Mathlib.Topology.MetricSpace.CantorScheme -public import Mathlib.Topology.MetricSpace.CauSeqFilter public import Mathlib.Topology.MetricSpace.Cauchy +public import Mathlib.Topology.MetricSpace.CauSeqFilter public import Mathlib.Topology.MetricSpace.Closeds public import Mathlib.Topology.MetricSpace.Completion public import Mathlib.Topology.MetricSpace.Congruence @@ -8027,6 +8097,7 @@ public import Mathlib.Topology.NhdsSet public import Mathlib.Topology.NhdsWithin public import Mathlib.Topology.NoetherianSpace public import Mathlib.Topology.OmegaCompletePartialOrder +public import Mathlib.Topology.OpenPartialHomeomorph public import Mathlib.Topology.OpenPartialHomeomorph.Basic public import Mathlib.Topology.OpenPartialHomeomorph.Composition public import Mathlib.Topology.OpenPartialHomeomorph.Constructions @@ -8050,8 +8121,8 @@ public import Mathlib.Topology.Order.Hom.Basic public import Mathlib.Topology.Order.Hom.Esakia public import Mathlib.Topology.Order.HullKernel public import Mathlib.Topology.Order.IntermediateValue -public import Mathlib.Topology.Order.IsLUB public import Mathlib.Topology.Order.IsLocallyClosed +public import Mathlib.Topology.Order.IsLUB public import Mathlib.Topology.Order.IsNormal public import Mathlib.Topology.Order.Lattice public import Mathlib.Topology.Order.LawsonTopology @@ -8089,6 +8160,7 @@ public import Mathlib.Topology.Semicontinuity.Basic public import Mathlib.Topology.Semicontinuity.Defs public import Mathlib.Topology.Semicontinuity.Hemicontinuity public import Mathlib.Topology.Semicontinuity.Lindelof +public import Mathlib.Topology.Semicontinuous public import Mathlib.Topology.SeparatedMap public import Mathlib.Topology.Separation.AlexandrovDiscrete public import Mathlib.Topology.Separation.Basic @@ -8123,23 +8195,23 @@ public import Mathlib.Topology.Sheaves.Forget public import Mathlib.Topology.Sheaves.Functors public import Mathlib.Topology.Sheaves.Init public import Mathlib.Topology.Sheaves.Limits -public import Mathlib.Topology.Sheaves.LocalPredicate public import Mathlib.Topology.Sheaves.LocallySurjective +public import Mathlib.Topology.Sheaves.LocalPredicate public import Mathlib.Topology.Sheaves.MayerVietoris public import Mathlib.Topology.Sheaves.Module public import Mathlib.Topology.Sheaves.Over -public import Mathlib.Topology.Sheaves.PUnit public import Mathlib.Topology.Sheaves.Points public import Mathlib.Topology.Sheaves.Presheaf public import Mathlib.Topology.Sheaves.PresheafOfFunctions +public import Mathlib.Topology.Sheaves.PUnit public import Mathlib.Topology.Sheaves.Sheaf public import Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts public import Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover public import Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections public import Mathlib.Topology.Sheaves.SheafCondition.Sites public import Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing -public import Mathlib.Topology.Sheaves.SheafOfFunctions public import Mathlib.Topology.Sheaves.Sheafify +public import Mathlib.Topology.Sheaves.SheafOfFunctions public import Mathlib.Topology.Sheaves.Skyscraper public import Mathlib.Topology.Sheaves.Stalks public import Mathlib.Topology.ShrinkingLemma @@ -8216,8 +8288,8 @@ public import Mathlib.Util.GetAllModules public import Mathlib.Util.LongNames public import Mathlib.Util.MemoFix public import Mathlib.Util.Notation3 -public import Mathlib.Util.PPOptions public import Mathlib.Util.ParseCommand +public import Mathlib.Util.PPOptions public import Mathlib.Util.PrintSorries public import Mathlib.Util.Qq public import Mathlib.Util.Simp @@ -8229,5 +8301,5 @@ public import Mathlib.Util.TermReduce public import Mathlib.Util.TransImports public import Mathlib.Util.WhatsNew public import Mathlib.Util.WithWeakNamespace - +public import Std set_option linter.style.longLine false diff --git a/Mathlib/Combinatorics/SimpleGraph/Action.lean b/Mathlib/Combinatorics/SimpleGraph/Action.lean new file mode 100644 index 00000000000000..0b7875c8109f46 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Action.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Maps +public import Mathlib.GroupTheory.GroupAction.Basic + +/-! +# Group actions on simple graphs + +Given a group `G` acting on a type `V` via `MulAction G V`, and a simple graph `Γ : SimpleGraph V`, +we say the action is a *graph action* if it preserves adjacency: `Γ.Adj u v → Γ.Adj (g • u) (g • v)` +for all `g : G`. + +## Main definitions + +* `GraphAction G Γ` — the action of `G` on `V` preserves the adjacency relation of `Γ` +* `GraphAction.adj_smul_iff` — for groups, adjacency is an iff (not just an implication) +* `GraphAction.toIso` — each `g : G` induces a graph isomorphism `Γ ≃g Γ` +* `IsVertexTransitive G Γ` — the action is a graph action and is transitive +* `IsArcTransitive G Γ` — the action is transitive on ordered adjacent pairs +* `IsLocallyTransitive G Γ v` — the stabilizer of `v` acts transitively on its neighbors + +## Main results + +* `isArcTransitive_of_vertexTransitive_locallyTransitive` — vertex-transitive + locally + transitive implies arc-transitive +-/ + +@[expose] public section + +variable {G V : Type*} + +/-- A group action on `V` is a *graph action* on `Γ : SimpleGraph V` if it preserves adjacency. -/ +class GraphAction (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop where + /-- The action preserves adjacency. -/ + adj_smul : ∀ (g : G) (u v : V), Γ.Adj u v → Γ.Adj (g • u) (g • v) + +namespace GraphAction + +variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [GraphAction G V Γ] + +/-- For group actions, adjacency is preserved in both directions: +`Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v`. -/ +theorem adj_smul_iff (g : G) (u v : V) : Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v := by + constructor + · intro h + have h' := adj_smul g⁻¹ (g • u) (g • v) h + simp only [inv_smul_smul] at h' + exact h' + · exact adj_smul g u v + +/-- Each group element `g` induces a graph isomorphism `Γ ≃g Γ`. -/ +noncomputable def toIso (g : G) : Γ ≃g Γ where + toEquiv := MulAction.toPerm g + map_rel_iff' := adj_smul_iff g _ _ + +@[simp] +theorem toIso_apply (g : G) (v : V) : (toIso g : Γ ≃g Γ) v = g • v := rfl + +@[simp] +theorem toIso_symm (g : G) : (toIso g : Γ ≃g Γ).symm = toIso g⁻¹ := by + ext v + simp [toIso] + +theorem toIso_mul (g h : G) : + (toIso (g * h) : Γ ≃g Γ) = (toIso h : Γ ≃g Γ).trans (toIso g) := by + ext v + simp [toIso, mul_smul] + +end GraphAction + +/-- A graph `Γ` is *vertex-transitive* under the action of `G` if `G` preserves adjacency +and acts transitively on the vertices. -/ +class IsVertexTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where + /-- The action is transitive on vertices. -/ + pretransitive : MulAction.IsPretransitive G V + +attribute [instance] IsVertexTransitive.pretransitive + +/-- A graph `Γ` is *arc-transitive* under the action of `G` if for any two arcs +`(u₁, v₁)` and `(u₂, v₂)`, there exists `g ∈ G` sending `u₁ ↦ u₂` and `v₁ ↦ v₂`. -/ +class IsArcTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where + /-- The action is transitive on arcs (ordered adjacent pairs). -/ + arc_transitive : ∀ u₁ v₁ u₂ v₂ : V, Γ.Adj u₁ v₁ → Γ.Adj u₂ v₂ → + ∃ g : G, g • u₁ = u₂ ∧ g • v₁ = v₂ + +namespace IsArcTransitive + +variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [IsArcTransitive G V Γ] + +/-- An arc-transitive graph with no isolated vertices is vertex-transitive. -/ +theorem isVertexTransitive (hne : ∀ v : V, ∃ w : V, Γ.Adj v w) : + IsVertexTransitive G V Γ where + pretransitive := ⟨by + intro x y + obtain ⟨x', hx'⟩ := hne x + obtain ⟨y', hy'⟩ := hne y + obtain ⟨g, hg, _⟩ := @arc_transitive G V _ _ Γ _ x x' y y' hx' hy' + exact ⟨g, hg⟩⟩ + +end IsArcTransitive + +/-- A graph is *locally transitive* at `v` if the stabilizer of `v` acts transitively +on the neighbors of `v`. -/ +def IsLocallyTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) (v : V) : Prop := + ∀ w₁ w₂ : V, Γ.Adj v w₁ → Γ.Adj v w₂ → + ∃ g : G, g • v = v ∧ g • w₁ = w₂ + +/-- A vertex-transitive, locally transitive graph is arc-transitive. -/ +theorem isArcTransitive_of_vertexTransitive_locallyTransitive + [Group G] [MulAction G V] (Γ : SimpleGraph V) [IsVertexTransitive G V Γ] + (hlocal : ∀ v : V, IsLocallyTransitive G V Γ v) : + IsArcTransitive G V Γ where + arc_transitive := by + intro u₁ v₁ u₂ v₂ h₁ h₂ + obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G u₁ u₂ + have hadj : Γ.Adj u₂ (g • v₁) := by + rw [← hg] + exact GraphAction.adj_smul g u₁ v₁ h₁ + obtain ⟨h, hhu₂, hhv⟩ := hlocal u₂ (g • v₁) v₂ hadj h₂ + exact ⟨h * g, by rw [mul_smul, hg, hhu₂], by rw [mul_smul, hhv]⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean new file mode 100644 index 00000000000000..c2ffaf6692651a --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Action +public import Mathlib.GroupTheory.GroupAction.Quotient +public import Mathlib.GroupTheory.DoubleCoset +public import Mathlib.Tactic.Group + +/-! +# Coset graphs (Sabidussi construction) + +Given a group `G`, a subgroup `H`, and a *connection set* `D ⊆ G` that is a union of +`(H, H)`-double cosets, is symmetric (`D = D⁻¹`), and is disjoint from `H`, we define the +**coset graph** `Sab(G, H, D)` whose vertices are the left cosets `G ⧸ H` and whose edges +connect `xH` to `yH` whenever `x⁻¹y ∈ D`. + +This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`, the coset graph on +`G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`. + +## Main definitions + +* `IsConnectionSet H D` — `D` is a union of `(H, H)`-double cosets, closed under inversion, + and disjoint from `H` +* `SimpleGraph.cosetGraph H D` — the coset graph `Sab(G, H, D)` as a `SimpleGraph (G ⧸ H)` + +## Main results + +* `SimpleGraph.cosetGraph.adj_mk` — adjacency is characterized by `x⁻¹y ∈ D` +* `SimpleGraph.cosetGraph.graphAction` — `G` acts on the coset graph preserving adjacency +* `SimpleGraph.cosetGraph.isVertexTransitive` — coset graphs are vertex-transitive + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2. +* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +/-- A set `D ⊆ G` is a *connection set* for the subgroup `H` if it is stable under +left and right multiplication by `H` (i.e., a union of `(H,H)`-double cosets), +is closed under inversion, and is disjoint from `H`. -/ +structure IsConnectionSet (H : Subgroup G) (D : Set G) : Prop where + /-- `D` is stable under left and right multiplication by elements of `H`. -/ + double_coset_stable : ∀ d ∈ D, ∀ h₁ ∈ (H : Set G), ∀ h₂ ∈ (H : Set G), h₁ * d * h₂ ∈ D + /-- `D` is closed under inversion. -/ + inv_mem : ∀ d ∈ D, d⁻¹ ∈ D + /-- `D` is disjoint from `H`. -/ + disjoint : Disjoint D ↑H + +namespace IsConnectionSet + +variable {H : Subgroup G} {D : Set G} + +theorem one_not_mem (hD : IsConnectionSet H D) : (1 : G) ∉ D := + fun h => Set.disjoint_left.mp hD.disjoint h (Subgroup.one_mem H) + +end IsConnectionSet + +/-- The **coset graph** `Sab(G, H, D)`. Vertices are the left cosets `G ⧸ H`, +and two cosets `xH, yH` are adjacent iff `x⁻¹y ∈ D`. + +This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`, +the coset graph on `G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`. -/ +noncomputable def SimpleGraph.cosetGraph (H : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) : SimpleGraph (G ⧸ H) where + Adj q₁ q₂ := Quotient.liftOn₂ q₁ q₂ (fun x y => x⁻¹ * y ∈ D) + (fun a₁ b₁ a₂ b₂ h₁ h₂ => by + have ha : a₁⁻¹ * a₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₁ + have hb : b₁⁻¹ * b₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₂ + apply propext; change a₁⁻¹ * b₁ ∈ D ↔ a₂⁻¹ * b₂ ∈ D; constructor + · intro h + have key : a₂⁻¹ * b₂ = (a₂⁻¹ * a₁) * (a₁⁻¹ * b₁) * (b₁⁻¹ * b₂) := by group + rw [key] + refine hD.double_coset_stable _ h _ ?_ _ hb + have : (a₁⁻¹ * a₂)⁻¹ ∈ (H : Set G) := H.inv_mem ha + rwa [mul_inv_rev, inv_inv] at this + · intro h + have key : a₁⁻¹ * b₁ = (a₁⁻¹ * a₂) * (a₂⁻¹ * b₂) * (b₂⁻¹ * b₁) := by group + rw [key] + refine hD.double_coset_stable _ h _ ha _ ?_ + have : (b₁⁻¹ * b₂)⁻¹ ∈ (H : Set G) := H.inv_mem hb + rwa [mul_inv_rev, inv_inv] at this) + symm := by + intro q₁ q₂ + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + simp only [Quotient.liftOn₂_mk] + intro h + have hmem := hD.inv_mem _ h + rwa [mul_inv_rev, inv_inv] at hmem + loopless := ⟨by + intro q + refine Quotient.inductionOn q fun x => ?_ + simp only [Quotient.liftOn₂_mk] + show ¬(x⁻¹ * x ∈ D) + rw [inv_mul_cancel] + exact hD.one_not_mem⟩ + +namespace SimpleGraph.cosetGraph + +variable (H : Subgroup G) (D : Set G) (hD : IsConnectionSet H D) + +/-- Adjacency in the coset graph is characterized by membership of `x⁻¹y` in `D`. -/ +@[simp] +theorem adj_mk (x y : G) : + (cosetGraph H D hD).Adj (QuotientGroup.mk x) (QuotientGroup.mk y) ↔ x⁻¹ * y ∈ D := + Iff.rfl + +/-- The left multiplication action of `G` on `G ⧸ H` preserves coset graph adjacency. -/ +instance graphAction : GraphAction G (G ⧸ H) (cosetGraph H D hD) where + adj_smul g q₁ q₂ := by + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + intro h + change (g * x)⁻¹ * (g * y) ∈ D + rw [mul_inv_rev, mul_assoc, inv_mul_cancel_left] + exact h + +/-- Coset graphs are vertex-transitive under the natural action of `G`. -/ +instance isVertexTransitive : IsVertexTransitive G (G ⧸ H) (cosetGraph H D hD) where + pretransitive := MulAction.isPretransitive_quotient G H + +end SimpleGraph.cosetGraph diff --git a/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean new file mode 100644 index 00000000000000..420b6dffab698e --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Symmetric +public import Mathlib.GroupTheory.GroupAction.Blocks + +/-! +# Quotient graphs and the Lorimer quotient theorem + +The quotient of a symmetric graph `Sab(G, H, HaH)` by a `G`-invariant partition +is again a symmetric graph `Sab(G, K, KaK)` for some overgroup `H ≤ K ≤ G`. + +## Main definitions + +* `SimpleGraph.quotientGraph` — quotient of a graph by a surjection (partition) +* `cosetQuotientMap` — the natural map `G ⧸ H → G ⧸ K` for `H ≤ K` +* `expandConnectionSet` — the expanded connection set `KDK` for an overgroup `K` + +## Main results + +* `quotient_cosetGraph_iso` — the quotient of `Sab(G,H,D)` is isomorphic to `Sab(G,K,KDK)` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §4. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +/-! ### Quotient graph construction -/ + +/-- The **quotient graph** of `Γ` with respect to a surjection `π : V → ι`. -/ +def SimpleGraph.quotientGraph {V ι : Type*} (Γ : SimpleGraph V) (π : V → ι) : + SimpleGraph ι where + Adj i j := i ≠ j ∧ ∃ u v : V, π u = i ∧ π v = j ∧ Γ.Adj u v + symm := by + intro i j ⟨hne, u, v, hui, hvj, hadj⟩ + exact ⟨hne.symm, v, u, hvj, hui, Γ.symm hadj⟩ + loopless := ⟨fun i ⟨hne, _⟩ => hne rfl⟩ + +/-! ### The coset quotient map -/ + +/-- The natural map `G ⧸ H → G ⧸ K` for `H ≤ K`, sending `gH ↦ gK`. -/ +noncomputable def cosetQuotientMap (H K : Subgroup G) (hHK : H ≤ K) : + G ⧸ H → G ⧸ K := + Quotient.map' id (fun _ _ h => QuotientGroup.leftRel_apply.mpr + (hHK (QuotientGroup.leftRel_apply.mp h))) + +@[simp] +theorem cosetQuotientMap_mk (H K : Subgroup G) (hHK : H ≤ K) (g : G) : + cosetQuotientMap H K hHK (QuotientGroup.mk g) = QuotientGroup.mk g := + rfl + +/-! ### Expanded connection set KDK -/ + +/-- The expanded connection set `KDK` for an overgroup `K`. -/ +def expandConnectionSet (K : Subgroup G) (D : Set G) : Set G := + {g : G | ∃ k₁ ∈ (K : Set G), ∃ d ∈ D, ∃ k₂ ∈ (K : Set G), g = k₁ * d * k₂} + +/-- `KDK` is a valid connection set for `K` when `D ∩ K = ∅`. -/ +theorem expandConnectionSet_isConnectionSet (H K : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) (hDK : Disjoint D ↑K) : + IsConnectionSet K (expandConnectionSet K D) where + double_coset_stable := by + intro d hd m₁ hm₁ m₂ hm₂ + obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd + exact ⟨m₁ * k₁, K.mul_mem hm₁ hk₁, e, he, k₂ * m₂, K.mul_mem hk₂ hm₂, by group⟩ + inv_mem := by + intro d hd + obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd + exact ⟨k₂⁻¹, K.inv_mem hk₂, e⁻¹, hD.inv_mem e he, k₁⁻¹, K.inv_mem hk₁, by group⟩ + disjoint := by + rw [Set.disjoint_left] + intro g hg hgK + obtain ⟨k₁, hk₁, d, hd, k₂, hk₂, rfl⟩ := hg + have : d ∈ (K : Set G) := by + have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hgK) (K.inv_mem hk₂) + convert this using 1; group + exact Set.disjoint_left.mp hDK hd this + +/-! ### The Lorimer quotient theorem -/ + +/-- **Lorimer's Quotient Theorem**: The quotient of `Sab(G, H, D)` by the overgroup +`K ≥ H` (with `D ∩ K = ∅`) is isomorphic to `Sab(G, K, KDK)`. + +The quotient map `G ⧸ H → G ⧸ K` (sending `gH ↦ gK`) induces a graph +isomorphism from the quotient graph to the coset graph with expanded +connection set. -/ +noncomputable def quotient_cosetGraph_iso (H K : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) (hHK : H ≤ K) + (hDK : Disjoint D ↑K) : + SimpleGraph.quotientGraph (SimpleGraph.cosetGraph H D hD) (cosetQuotientMap H K hHK) ≃g + SimpleGraph.cosetGraph K (expandConnectionSet K D) + (expandConnectionSet_isConnectionSet H K D hD hDK) where + toEquiv := Equiv.refl _ + map_rel_iff' := by + intro q₁ q₂ + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + simp only [Equiv.refl_apply] + rw [SimpleGraph.cosetGraph.adj_mk] + constructor + · intro ⟨k₁, hk₁, d, hd, k₂, hk₂, heq⟩ + refine ⟨?_, QuotientGroup.mk (x * k₁), + QuotientGroup.mk (x * k₁ * d), ?_, ?_, ?_⟩ + · intro heq' + have : d ∈ (K : Set G) := by + have hK : k₁ * d * k₂ ∈ (K : Set G) := heq ▸ QuotientGroup.eq.mp heq' + have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hK) (K.inv_mem hk₂) + convert this using 1; group + exact Set.disjoint_left.mp hDK hd this + · simp only [cosetQuotientMap_mk, QuotientGroup.eq] + have : (x * k₁)⁻¹ * x = k₁⁻¹ := by group + rw [this]; exact K.inv_mem hk₁ + · simp only [cosetQuotientMap_mk, QuotientGroup.eq] + have hy : y = x * (k₁ * d * k₂) := by rw [← heq]; group + have : (x * k₁ * d)⁻¹ * (x * (k₁ * d * k₂)) = k₂ := by group + rw [hy, this]; exact hk₂ + · convert hd using 1 + simp [mul_inv_rev, mul_assoc, inv_mul_cancel_left] + · intro ⟨_, u, v, hu, hv, hadj⟩ + revert hu hv hadj + refine Quotient.inductionOn₂ u v fun x' y' hx' hy' (hadj : x'⁻¹ * y' ∈ D) => ?_ + simp only [cosetQuotientMap_mk] at hx' hy' + have hxK : x⁻¹ * x' ∈ (K : Set G) := by + have := K.inv_mem (QuotientGroup.eq.mp hx' : x'⁻¹ * x ∈ K) + rwa [mul_inv_rev, inv_inv] at this + have hyK : y'⁻¹ * y ∈ (K : Set G) := QuotientGroup.eq.mp hy' + exact ⟨x⁻¹ * x', hxK, x'⁻¹ * y', hadj, y'⁻¹ * y, hyK, by group⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/Representation.lean b/Mathlib/Combinatorics/SimpleGraph/Representation.lean new file mode 100644 index 00000000000000..b1faf6b2f9bd21 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Representation.lean @@ -0,0 +1,163 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.CosetGraph +public import Mathlib.GroupTheory.GroupAction.Quotient +public import Mathlib.Tactic.Group + +/-! +# The Sabidussi representation theorem + +Every vertex-transitive graph is isomorphic to a coset graph. More precisely, +if `G` acts vertex-transitively on a graph `Γ`, then for any basepoint `v`, +the orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph +isomorphism from `Γ` to `Sab(G, Gᵥ, D)`, where `D = {g ∈ G : Γ.Adj v (g • v)}`. + +## Main definitions + +* `connectionSet G Γ v` — the set of group elements moving `v` to a neighbor +* `connectionSet.isConnectionSet` — the connection set satisfies the axioms +* `sabidussiEquiv` — the equivalence `V ≃ G ⧸ stabilizer G v` for transitive actions +* `sabidussiIso` — the graph isomorphism `Γ ≃g cosetGraph (stabilizer G v) D` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2. +* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438. +-/ + +@[expose] public section + +variable {G V : Type*} [Group G] [MulAction G V] {Γ : SimpleGraph V} + +/-! ### The connection set -/ + +/-- The *connection set* of a basepoint `v`: the set of group elements +that move `v` to one of its neighbors. -/ +def connectionSet (G : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) (v : V) : Set G := + {g : G | Γ.Adj v (g • v)} + +namespace connectionSet + +variable [GraphAction G V Γ] (v : V) + +omit [GraphAction G V Γ] in +theorem one_not_mem : (1 : G) ∉ connectionSet G Γ v := by + simp [connectionSet] + +theorem inv_mem {g : G} (hg : g ∈ connectionSet G Γ v) : + g⁻¹ ∈ connectionSet G Γ v := by + simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢ + have h := Γ.symm hg + rwa [← GraphAction.adj_smul_iff g⁻¹, inv_smul_smul] at h + +theorem double_coset_stable {g : G} (hg : g ∈ connectionSet G Γ v) + {h₁ : G} (hh₁ : h₁ ∈ MulAction.stabilizer G v) + {h₂ : G} (hh₂ : h₂ ∈ MulAction.stabilizer G v) : + h₁ * g * h₂ ∈ connectionSet G Γ v := by + simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢ + rw [mul_smul, mul_smul, MulAction.mem_stabilizer_iff.mp hh₂] + have := GraphAction.adj_smul h₁ v (g • v) hg + rwa [MulAction.mem_stabilizer_iff.mp hh₁] at this + +omit [GraphAction G V Γ] in +theorem disjoint_stabilizer : + Disjoint (connectionSet G Γ v) ↑(MulAction.stabilizer G v) := by + rw [Set.disjoint_left] + intro g hg hstab + simp only [connectionSet, Set.mem_setOf_eq] at hg + rw [SetLike.mem_coe, MulAction.mem_stabilizer_iff] at hstab + rw [hstab] at hg + exact (Γ.loopless.irrefl v) hg + +/-- The connection set forms a valid `IsConnectionSet` for the stabilizer subgroup. -/ +theorem isConnectionSet : + IsConnectionSet (MulAction.stabilizer G v) (connectionSet G Γ v) where + double_coset_stable _ hd _ hh₁ _ hh₂ := double_coset_stable v hd hh₁ hh₂ + inv_mem _ hd := inv_mem v hd + disjoint := disjoint_stabilizer v + +end connectionSet + +/-! ### The orbit-stabilizer equivalence -/ + +section SabidussiRepresentation + +variable [GraphAction G V Γ] [MulAction.IsPretransitive G V] (v : V) + +/-- The equivalence `V ≃ G ⧸ stabilizer G v` for a transitive action. + +The forward map sends `u` to the coset `gH` where `g • v = u`. +The inverse map sends `⟦g⟧` to `g • v`. -/ +noncomputable def sabidussiEquiv : V ≃ G ⧸ MulAction.stabilizer G v where + toFun u := QuotientGroup.mk (MulAction.exists_smul_eq G v u).choose + invFun := Quotient.lift (· • v) (by + intro a b hab + have hmem : (a⁻¹ * b) • v = v := + MulAction.mem_stabilizer_iff.mp (QuotientGroup.leftRel_apply.mp hab) + calc a • v = a • ((a⁻¹ * b) • v) := by rw [hmem] + _ = (a * (a⁻¹ * b)) • v := (mul_smul a (a⁻¹ * b) v).symm + _ = b • v := by rw [mul_inv_cancel_left]) + left_inv u := by + simp only + exact (MulAction.exists_smul_eq G v u).choose_spec + right_inv := by + intro q + refine Quotient.inductionOn q fun g => ?_ + simp only [Quotient.lift_mk] + apply QuotientGroup.eq.mpr + rw [MulAction.mem_stabilizer_iff, mul_smul] + set g' := (MulAction.exists_smul_eq G v (g • v)).choose + have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec + calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec] + _ = v := inv_smul_smul g' v + +@[simp] +theorem sabidussiEquiv_smul (g : G) : + sabidussiEquiv v (g • v) = (g : G ⧸ MulAction.stabilizer G v) := by + simp only [sabidussiEquiv] + apply QuotientGroup.eq.mpr + rw [MulAction.mem_stabilizer_iff, mul_smul] + set g' := (MulAction.exists_smul_eq G v (g • v)).choose + have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec + calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec] + _ = v := inv_smul_smul g' v + +@[simp] +theorem sabidussiEquiv_symm_mk (g : G) : + (sabidussiEquiv v).symm (QuotientGroup.mk g) = g • v := by + rfl + +/-- **Sabidussi's Representation Theorem**: Every vertex-transitive graph is +isomorphic to a coset graph. + +The orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph isomorphism +from `Γ` to `cosetGraph (stabilizer G v) (connectionSet G Γ v)`. -/ +noncomputable def sabidussiIso : + Γ ≃g SimpleGraph.cosetGraph (MulAction.stabilizer G v) + (connectionSet G Γ v) (connectionSet.isConnectionSet v) where + toEquiv := sabidussiEquiv v + map_rel_iff' := by + intro u w + set g₁ := (MulAction.exists_smul_eq G v u).choose + set g₂ := (MulAction.exists_smul_eq G v w).choose + have hu : g₁ • v = u := (MulAction.exists_smul_eq G v u).choose_spec + have hw : g₂ • v = w := (MulAction.exists_smul_eq G v w).choose_spec + change g₁⁻¹ * g₂ ∈ connectionSet G Γ v ↔ Γ.Adj u w + rw [← hu, ← hw] + simp only [connectionSet, Set.mem_setOf_eq, mul_smul] + constructor + · intro h + have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mp + (by rwa [inv_smul_smul]) + exact this + · intro h + have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mpr h + rwa [inv_smul_smul] at this + +end SabidussiRepresentation diff --git a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean new file mode 100644 index 00000000000000..396baa0b54a598 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Representation +public import Mathlib.GroupTheory.DoubleCoset +public import Mathlib.Tactic.Group + +/-! +# Symmetric graphs and Lorimer's theorem + +A *symmetric* (arc-transitive) graph is a coset graph `Sab(G, H, HaH)` where `a` is an +involution not in `H`. This file proves both directions of Lorimer's theorem: +the forward direction shows `Sab(G, H, HaH)` is arc-transitive when `a² = 1` and `a ∉ H`, +and the reverse direction shows every arc-transitive graph's connection set is a single +double coset `HaH` where `a` swaps an arc. + +## Main definitions + +* `doubleCoset_isConnectionSet` — `HaH` is a valid connection set when `a² = 1, a ∉ H` +* `sabidussiSymmetricGraph` — the coset graph `Sab(G, H, HaH)` + +## Main results + +* `lorimer_forward` — `Sab(G, H, HaH)` is arc-transitive when `a² = 1, a ∉ H` +* `connectionSet_eq_doubleCoset` — under arc-transitivity, the connection set is a single + double coset +* `lorimer_reverse` — every arc-transitive graph has an arc-swapping involution `a` with + `a ∉ Gᵥ`, `a² ∈ Gᵥ`, and `D = GᵥaGᵥ` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §§3–4. +* Lorimer, *Vertex-transitive graphs*, 1984. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +private theorem inv_eq_self_of_sq_eq_one {a : G} (ha : a ^ 2 = 1) : a⁻¹ = a := + inv_eq_of_mul_eq_one_left (by rwa [← sq]) + +open DoubleCoset in +/-- `HaH` is a valid connection set when `a² = 1` and `a ∉ H`. -/ +theorem doubleCoset_isConnectionSet (H : Subgroup G) (a : G) + (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H) : + IsConnectionSet H (doubleCoset a (H : Set G) H) where + double_coset_stable := by + intro d hd k₁ hk₁ k₂ hk₂ + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd + exact mem_doubleCoset.mpr + ⟨k₁ * h₁, H.mul_mem hk₁ hh₁, h₂ * k₂, H.mul_mem hh₂ hk₂, by group⟩ + inv_mem := by + intro d hd + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd + have ha_inv := inv_eq_self_of_sq_eq_one ha_sq + refine mem_doubleCoset.mpr ⟨h₂⁻¹, H.inv_mem hh₂, h₁⁻¹, H.inv_mem hh₁, ?_⟩ + calc (h₁ * a * h₂)⁻¹ = h₂⁻¹ * a⁻¹ * h₁⁻¹ := by group + _ = h₂⁻¹ * a * h₁⁻¹ := by rw [ha_inv] + disjoint := by + rw [Set.disjoint_left] + intro g hg hgH + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hg + have : a = h₁⁻¹ * (h₁ * a * h₂) * h₂⁻¹ := by group + rw [this] at ha_not + exact ha_not (H.mul_mem (H.mul_mem (H.inv_mem hh₁) hgH) (H.inv_mem hh₂)) + +section Lorimer + +variable (H : Subgroup G) (a : G) (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H) + +/-- The coset graph `Sab(G, H, HaH)` for an involution `a ∉ H`. -/ +noncomputable abbrev sabidussiSymmetricGraph := + SimpleGraph.cosetGraph H (DoubleCoset.doubleCoset a (H : Set G) H) + (doubleCoset_isConnectionSet H a ha_sq ha_not) + +/-- Local transitivity at the identity coset. -/ +private theorem locallyTransitive_at_one : + IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) + ((1 : G) : G ⧸ H) := by + intro w₁ w₂ hw₁ hw₂ + revert hw₁ hw₂ + refine Quotient.inductionOn₂ w₁ w₂ fun y₁ y₂ hy₁ hy₂ => ?_ + change (1 : G)⁻¹ * y₁ ∈ _ at hy₁; change (1 : G)⁻¹ * y₂ ∈ _ at hy₂ + simp only [inv_one, one_mul] at hy₁ hy₂ + obtain ⟨h₁, hh₁, k₁, hk₁, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₁ + obtain ⟨h₂, hh₂, k₂, hk₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₂ + refine ⟨h₂ * h₁⁻¹, ?_, ?_⟩ + · change (h₂ * h₁⁻¹) • ((1 : G) : G ⧸ H) = (1 : G) + rw [MulAction.Quotient.smul_coe, smul_eq_mul, mul_one] + apply QuotientGroup.eq.mpr + show (h₂ * h₁⁻¹)⁻¹ * 1 ∈ H + simp only [mul_one, mul_inv_rev, inv_inv] + exact H.mul_mem hh₁ (H.inv_mem hh₂) + · change (h₂ * h₁⁻¹) • ((h₁ * a * k₁ : G) : G ⧸ H) = (h₂ * a * k₂ : G) + rw [MulAction.Quotient.smul_coe, smul_eq_mul, QuotientGroup.eq] + have ha_inv := inv_eq_self_of_sq_eq_one ha_sq + suffices h : (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂) = k₁⁻¹ * k₂ by + rw [h]; exact H.mul_mem (H.inv_mem hk₁) hk₂ + calc (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂) + = (h₂ * a * k₁)⁻¹ * (h₂ * a * k₂) := by congr 1; group + _ = k₁⁻¹ * a⁻¹ * (h₂⁻¹ * (h₂ * a * k₂)) := by group + _ = k₁⁻¹ * a⁻¹ * (a * k₂) := by rw [show h₂⁻¹ * (h₂ * a * k₂) = a * k₂ from by group] + _ = k₁⁻¹ * (a⁻¹ * a) * k₂ := by group + _ = k₁⁻¹ * k₂ := by rw [ha_inv]; simp [← sq, ha_sq] + +/-- Local transitivity at any vertex, transported from `⟦1⟧`. -/ +private theorem locallyTransitive_everywhere : + ∀ q : G ⧸ H, + IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) q := by + intro q w₁ w₂ hw₁ hw₂ + set Γ := sabidussiSymmetricGraph H a ha_sq ha_not + obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G ((1 : G) : G ⧸ H) q + have hw₁' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₁) := by + have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₁).mpr hw₁ + rwa [← hg, inv_smul_smul] at this + have hw₂' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₂) := by + have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₂).mpr hw₂ + rwa [← hg, inv_smul_smul] at this + obtain ⟨h, hfix, hsend⟩ := + locallyTransitive_at_one H a ha_sq ha_not (g⁻¹ • w₁) (g⁻¹ • w₂) hw₁' hw₂' + refine ⟨g * h * g⁻¹, ?_, ?_⟩ + · calc (g * h * g⁻¹) • q = g • (h • (g⁻¹ • q)) := by simp [mul_smul] + _ = g • (h • ((1 : G) : G ⧸ H)) := by rw [← hg, inv_smul_smul] + _ = g • ((1 : G) : G ⧸ H) := by rw [hfix] + _ = q := hg + · calc (g * h * g⁻¹) • w₁ = g • (h • (g⁻¹ • w₁)) := by simp [mul_smul] + _ = g • (g⁻¹ • w₂) := by rw [hsend] + _ = w₂ := smul_inv_smul g w₂ + +/-- **Lorimer's Theorem (forward direction)**: `Sab(G, H, HaH)` is arc-transitive +when `a² = 1` and `a ∉ H`. -/ +theorem lorimer_forward : + IsArcTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) := + isArcTransitive_of_vertexTransitive_locallyTransitive _ + (locallyTransitive_everywhere H a ha_sq ha_not) + +end Lorimer + +/-! ### Lorimer's theorem (reverse direction) -/ + +/-- Under arc-transitivity, the stabilizer acts transitively on neighbors. -/ +theorem stabilizer_transitive_on_neighbors {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v : V) {w u : V} (hw : Γ.Adj v w) (hu : Γ.Adj v u) : + ∃ h ∈ MulAction.stabilizer G v, h • w = u := by + obtain ⟨g, hgv, hgw⟩ := @IsArcTransitive.arc_transitive G V _ _ Γ _ v w v u hw hu + exact ⟨g, MulAction.mem_stabilizer_iff.mpr hgv, hgw⟩ + +/-- Under arc-transitivity, the connection set is a single double coset `HaH`. -/ +theorem connectionSet_eq_doubleCoset {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v : V) {a : G} (ha : a ∈ connectionSet G Γ v) : + connectionSet G Γ v = + DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G) + (MulAction.stabilizer G v) := by + ext g + constructor + · intro hg + obtain ⟨h, hh, hhw⟩ := @stabilizer_transitive_on_neighbors G _ V _ Γ _ v _ _ ha hg + rw [DoubleCoset.mem_doubleCoset] + exact ⟨h, hh, (g⁻¹ * (h * a))⁻¹, + (MulAction.stabilizer G v).inv_mem (by + rw [MulAction.mem_stabilizer_iff, mul_smul, mul_smul, hhw, inv_smul_smul]), + by group⟩ + · intro hg + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hg + exact connectionSet.double_coset_stable v ha hh₁ hh₂ + +/-- **Lorimer's Theorem (reverse direction)**: Every arc-transitive graph's connection +set is a single `(H,H)`-double coset, determined by the arc-swapping element. + +Combined with `sabidussiIso`, this shows every arc-transitive graph +is `Sab(G, stabilizer G v, HaH)` where `a` swaps an arc `(v,w)`. -/ +theorem lorimer_reverse {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v w : V) (hvw : Γ.Adj v w) : + ∃ a : G, a • v = w ∧ a • w = v ∧ a ∉ MulAction.stabilizer G v ∧ + a ^ 2 ∈ MulAction.stabilizer G v ∧ + connectionSet G Γ v = + DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G) + (MulAction.stabilizer G v) := by + obtain ⟨a, hav, haw⟩ := + @IsArcTransitive.arc_transitive G V _ _ Γ _ v w w v hvw (Γ.symm hvw) + refine ⟨a, hav, haw, ?_, ?_, ?_⟩ + · intro hmem + rw [MulAction.mem_stabilizer_iff] at hmem + rw [hmem] at hav + exact Γ.loopless.irrefl v (hav ▸ hvw) + · rw [MulAction.mem_stabilizer_iff, sq, mul_smul, hav, haw] + · exact connectionSet_eq_doubleCoset Γ v (by + simp only [connectionSet, Set.mem_setOf_eq, hav]; exact hvw)