diff --git a/Archive.lean b/Archive.lean index 990ddbc04a894f..bbc9b7e6a08528 100644 --- a/Archive.lean +++ b/Archive.lean @@ -62,6 +62,7 @@ import Archive.Imo.Imo2024Q5 import Archive.Imo.Imo2024Q6 import Archive.Imo.Imo2025Q3 import Archive.Kuratowski +import Archive.LangerGraph import Archive.MinimalSheffer import Archive.MiuLanguage.Basic import Archive.MiuLanguage.DecisionNec diff --git a/Archive/LangerGraph.lean b/Archive/LangerGraph.lean new file mode 100644 index 00000000000000..21f39c3472a1a1 --- /dev/null +++ b/Archive/LangerGraph.lean @@ -0,0 +1,775 @@ +/- +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.Data.ZMod.Basic +import Mathlib.Data.Matrix.Basic +import Mathlib.Data.Fin.VecNotation +import Mathlib.Combinatorics.SimpleGraph.Basic +import Mathlib.Combinatorics.SimpleGraph.Action +import Mathlib.Combinatorics.SimpleGraph.Representation + +/-! +# The Langer graph, the Tutte 12-cage, and the GH(2,2) ecosystem + +The **Langer graph** is the collinearity graph of the split Cayley hexagon GH(2,2), +the unique generalized 6-gon over 𝔽₂. It has 63 vertices (the points of the parabolic +quadric Q(6,2) in PG(6,2)), is 6-regular with 189 edges, and is the unique +distance-regular graph with intersection array {6, 4, 4; 1, 1, 3}. + +The **Tutte 12-cage** is the incidence graph of GH(2,2): 126 vertices +(63 points + 63 lines), 189 edges, girth 12. It is semisymmetric — edge-transitive +but not vertex-transitive — because no polarity exists for GH(2,2) over 𝔽₂. + +The main result `langer_eq_tutte12_distance2` proves that the Langer graph (defined +algebraically via the Zorn product on Q(6,2)) equals the distance-2 graph of the +Tutte 12-cage restricted to points (defined combinatorially from the edge list). +The proof uses G₂(2) transitivity: both graphs are invariant under two generators +of G₂(2), so they agree everywhere if they agree at vertex 0. + +## Main definitions + +* `langerSimpleGraph` — the Langer graph on `Fin 63`, via Zorn product +* `tutte12CageGraph` — the Tutte 12-cage on `Fin 126`, via edge list +* `Q62form` — the quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷ +* `Q62_H` — the 7 × 63 parity-check matrix from Q(6,2) + +## Main results + +* `Q62_self_orthogonal` — H · Hᵀ = 0 over 𝔽₂ +* `langer_regular` — the Langer graph is 6-regular +* `tutte12_bipartite` — the Tutte 12-cage is bipartite +* `langer_eq_tutte12_distance2'` — algebraic Langer = geometric distance-2 + (structural proof via G₂(2) transitivity) + +## Visualizations + +* [The Langer graph](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/langer-63v.jpg) — symmetry-aware drawing with 6-fold rotational layout +* [The Tutte 12-cage](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/tutte-12cage.jpg) — incidence graph of GH(2,2) + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798 +* Benson, *Minimal regular graphs of girth 8 and 12*, Canad. J. Math. 18 (1966) +* Springer–Veldkamp, *Octonions, Jordan Algebras and Exceptional Groups*, §1.8 +-/ + +set_option linter.style.nativeDecide false + +open Matrix + +/-! ## Part 1: The quadratic form Q(6,2) -/ + +/-- The quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷. +Points of Q(6,2) are the nonzero vectors with Q(x) = 0. -/ +def Q62form (x : Fin 7 → ZMod 2) : ZMod 2 := + x 0 * x 4 + x 1 * x 5 + x 2 * x 6 + x 3 * x 3 + +/-- Convert a natural number (1..127) to its bit vector in 𝔽₂⁷. -/ +def toBitVec (n : Fin 128) : Fin 7 → ZMod 2 := + fun i => if n.val / (2 ^ i.val) % 2 = 0 then 0 else 1 + +/-- The list of indices (1..127) whose bit vectors lie on Q(6,2). -/ +def q62Indices : List (Fin 128) := + (List.finRange 128).tail.filter fun n => Q62form (toBitVec n) = 0 + +/-- Q(6,2) has exactly 63 points. -/ +theorem q62_card : q62Indices.length = 63 := by native_decide + +/-- Get the n-th point of Q(6,2) (as an index into Fin 128). -/ +def q62Point (j : Fin 63) : Fin 128 := + q62Indices.get (j.cast (by native_decide)) + +/-- The parity-check matrix: H[i][j] = (j-th Q(6,2) point)[i-th coordinate]. -/ +def Q62_H : Matrix (Fin 7) (Fin 63) (ZMod 2) := + fun i j => toBitVec (q62Point j) i + +/-- **Self-orthogonality of Q(6,2)**: H · Hᵀ = 0 over 𝔽₂. +The CSS condition: the code C = ker(H) contains its dual C⊥ = rowspan(H). -/ +theorem Q62_self_orthogonal : Q62_H * Q62_Hᵀ = (0 : Matrix (Fin 7) (Fin 7) (ZMod 2)) := by + native_decide + +/-! ## Part 2: The Langer graph via Zorn product -/ + +/-- Adjacency test for the Langer graph via the Zorn product criterion. +Returns `true` iff `i ≠ j` and all eight entries of M_x · M_y vanish, +where M_x is the Zorn vector matrix of the split octonion algebra over 𝔽₂. -/ +def langerAdjBool (i j : Fin 63) : Bool := + if i == j then false else + let x := toBitVec (q62Point i) + let y := toBitVec (q62Point j) + let α := x 3; let γ := y 3 + (α * γ + x 0 * y 4 + x 1 * y 5 + x 2 * y 6 == 0) && + (α * γ + x 4 * y 0 + x 5 * y 1 + x 6 * y 2 == 0) && + (γ * x 0 + α * y 0 + x 5 * y 6 + x 6 * y 5 == 0) && + (γ * x 1 + α * y 1 + x 6 * y 4 + x 4 * y 6 == 0) && + (γ * x 2 + α * y 2 + x 4 * y 5 + x 5 * y 4 == 0) && + (γ * x 4 + α * y 4 + x 1 * y 2 + x 2 * y 1 == 0) && + (γ * x 5 + α * y 5 + x 2 * y 0 + x 0 * y 2 == 0) && + (γ * x 6 + α * y 6 + x 0 * y 1 + x 1 * y 0 == 0) + +/-- The **Langer graph**: collinearity graph of the split Cayley hexagon GH(2,2) +on the 63 points of Q(6,2). 6-regular, 189 edges, distance-regular with +intersection array {6, 4, 4; 1, 1, 3}. Aut ≅ G₂(2) of order 12096. -/ +def langerSimpleGraph : SimpleGraph (Fin 63) where + Adj i j := langerAdjBool i j + symm i j := by simp only [langerAdjBool]; revert i j; native_decide + loopless := ⟨fun i => by simp only [langerAdjBool]; revert i; native_decide⟩ + +instance langerDecAdj : DecidableRel langerSimpleGraph.Adj := + fun i j => inferInstanceAs (Decidable (langerAdjBool i j)) + +/-- The Langer graph is 6-regular. -/ +theorem langer_regular : + ∀ v : Fin 63, (Finset.univ.filter fun w => langerSimpleGraph.Adj v w).card = 6 := by + native_decide + +/-- The Langer graph has 189 undirected edges. -/ +theorem langer_edges : + (Finset.univ.filter fun p : Fin 63 × Fin 63 => + p.1 < p.2 ∧ langerSimpleGraph.Adj p.1 p.2).card = 189 := by + native_decide + +/-! ## Part 3: The Tutte 12-cage -/ + +/-- Edge list for the Tutte 12-cage (189 edges, 0-indexed). +Vertices 0–62 are points of GH(2,2), vertices 63–125 are lines. +Every edge connects a point to a line (bipartite). -/ +private def tutte12Edges : Array (Fin 126 × Fin 126) := #[ + (0,63), (0,64), (0,65), (1,66), (1,67), (1,68), + (2,69), (2,70), (2,71), (3,72), (3,73), (3,74), + (4,75), (4,76), (4,77), (5,78), (5,79), (5,80), + (6,81), (6,82), (6,83), (7,66), (7,72), (7,78), + (8,66), (8,84), (8,85), (9,72), (9,86), (9,87), + (10,78), (10,88), (10,89), (11,90), (11,91), (11,92), + (12,93), (12,94), (12,95), (13,96), (13,97), (13,98), + (14,99), (14,100), (14,101), (15,63), (15,73), (15,75), + (16,63), (16,102), (16,103), (17,73), (17,90), (17,96), + (18,75), (18,104), (18,105), (19,86), (19,106), (19,107), + (20,99), (20,108), (20,109), (21,87), (21,110), (21,111), + (22,93), (22,112), (22,113), (23,69), (23,74), (23,81), + (24,69), (24,114), (24,115), (25,74), (25,93), (25,99), + (26,81), (26,116), (26,117), (27,96), (27,118), (27,119), + (28,87), (28,120), (28,121), (29,90), (29,122), (29,123), + (30,86), (30,124), (30,125), (31,64), (31,67), (31,70), + (32,64), (32,106), (32,108), (33,67), (33,91), (33,94), + (34,70), (34,118), (34,120), (35,84), (35,102), (35,114), + (36,100), (36,103), (36,124), (37,85), (37,112), (37,122), + (38,97), (38,110), (38,115), (39,68), (39,76), (39,82), + (40,68), (40,97), (40,100), (41,76), (41,107), (41,113), + (42,82), (42,121), (42,123), (43,94), (43,104), (43,125), + (44,91), (44,111), (44,116), (45,85), (45,105), (45,117), + (46,84), (46,109), (46,119), (47,65), (47,79), (47,83), + (48,65), (48,110), (48,112), (49,79), (49,92), (49,101), + (50,83), (50,119), (50,125), (51,88), (51,108), (51,123), + (52,98), (52,106), (52,117), (53,89), (53,103), (53,116), + (54,95), (54,102), (54,121), (55,71), (55,77), (55,80), + (56,71), (56,122), (56,124), (57,77), (57,109), (57,111), + (58,80), (58,95), (58,98), (59,101), (59,105), (59,120), + (60,89), (60,113), (60,118), (61,88), (61,104), (61,115), + (62,92), (62,107), (62,114)] + +private def tutte12AdjBool (u v : Fin 126) : Bool := + tutte12Edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **Tutte 12-cage**: incidence graph of GH(2,2) on 126 vertices. +3-regular, 189 edges, girth 12. Semisymmetric (edge-transitive, not vertex-transitive). -/ +def tutte12CageGraph : SimpleGraph (Fin 126) where + Adj u v := tutte12AdjBool u v + symm u v := by simp only [tutte12AdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [tutte12AdjBool]; revert u; native_decide⟩ + +instance tutte12DecAdj : DecidableRel tutte12CageGraph.Adj := + fun u v => inferInstanceAs (Decidable (tutte12AdjBool u v)) + +/-- The Tutte 12-cage is 3-regular. -/ +theorem tutte12_regular : + ∀ v : Fin 126, (Finset.univ.filter fun w => tutte12CageGraph.Adj v w).card = 3 := by + native_decide + +/-- The bipartition: point (< 63) or line (≥ 63). -/ +def tutte12Side (v : Fin 126) : Fin 2 := + if v.val < 63 then 0 else 1 + +/-- The Tutte 12-cage is bipartite: every edge connects a point to a line. -/ +theorem tutte12_bipartite : + ∀ u v : Fin 126, tutte12CageGraph.Adj u v → tutte12Side u ≠ tutte12Side v := by + native_decide + +/-! ## Part 4: Distance-2 adjacency on points -/ + +/-- Distance-2 adjacency on points: p ~ q iff they share a line vertex +in the Tutte 12-cage. -/ +def tutte12Distance2Bool (p q : Fin 63) : Bool := + p != q && + let pv : Fin 126 := ⟨p.val, by omega⟩ + let qv : Fin 126 := ⟨q.val, by omega⟩ + (List.finRange 63).any fun l => + let lv : Fin 126 := ⟨l.val + 63, by omega⟩ + tutte12AdjBool pv lv && tutte12AdjBool qv lv + +/-! ## Part 5: G₂(2) generators and invariance -/ + +private def g2gen1Fwd : Array (Fin 63) := #[ + ⟨1, by omega⟩, ⟨3, by omega⟩, ⟨5, by omega⟩, ⟨2, by omega⟩, ⟨0, by omega⟩, + ⟨6, by omega⟩, ⟨4, by omega⟩, ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨24, by omega⟩, + ⟨26, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩, ⟨27, by omega⟩, ⟨29, by omega⟩, + ⟨31, by omega⟩, ⟨33, by omega⟩, ⟨34, by omega⟩, ⟨32, by omega⟩, ⟨35, by omega⟩, + ⟨37, by omega⟩, ⟨38, by omega⟩, ⟨36, by omega⟩, ⟨55, by omega⟩, ⟨58, by omega⟩, + ⟨56, by omega⟩, ⟨57, by omega⟩, ⟨60, by omega⟩, ⟨61, by omega⟩, ⟨59, by omega⟩, + ⟨62, by omega⟩, ⟨7, by omega⟩, ⟨8, by omega⟩, ⟨9, by omega⟩, ⟨10, by omega⟩, + ⟨12, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩, + ⟨17, by omega⟩, ⟨16, by omega⟩, ⟨18, by omega⟩, ⟨19, by omega⟩, ⟨21, by omega⟩, + ⟨20, by omega⟩, ⟨22, by omega⟩, ⟨39, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩, + ⟨41, by omega⟩, ⟨45, by omega⟩, ⟨46, by omega⟩, ⟨44, by omega⟩, ⟨43, by omega⟩, + ⟨47, by omega⟩, ⟨49, by omega⟩, ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨51, by omega⟩, + ⟨53, by omega⟩, ⟨52, by omega⟩, ⟨54, by omega⟩] + +private def g2gen1Inv : Array (Fin 63) := #[ + ⟨4, by omega⟩, ⟨0, by omega⟩, ⟨3, by omega⟩, ⟨1, by omega⟩, ⟨6, by omega⟩, + ⟨2, by omega⟩, ⟨5, by omega⟩, ⟨31, by omega⟩, ⟨32, by omega⟩, ⟨33, by omega⟩, + ⟨34, by omega⟩, ⟨36, by omega⟩, ⟨35, by omega⟩, ⟨38, by omega⟩, ⟨37, by omega⟩, + ⟨39, by omega⟩, ⟨41, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩, ⟨43, by omega⟩, + ⟨45, by omega⟩, ⟨44, by omega⟩, ⟨46, by omega⟩, ⟨7, by omega⟩, ⟨9, by omega⟩, + ⟨8, by omega⟩, ⟨10, by omega⟩, ⟨13, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩, + ⟨12, by omega⟩, ⟨15, by omega⟩, ⟨18, by omega⟩, ⟨16, by omega⟩, ⟨17, by omega⟩, + ⟨19, by omega⟩, ⟨22, by omega⟩, ⟨20, by omega⟩, ⟨21, by omega⟩, ⟨47, by omega⟩, + ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨49, by omega⟩, ⟨54, by omega⟩, ⟨53, by omega⟩, + ⟨51, by omega⟩, ⟨52, by omega⟩, ⟨55, by omega⟩, ⟨57, by omega⟩, ⟨56, by omega⟩, + ⟨58, by omega⟩, ⟨59, by omega⟩, ⟨61, by omega⟩, ⟨60, by omega⟩, ⟨62, by omega⟩, + ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨26, by omega⟩, ⟨24, by omega⟩, ⟨29, by omega⟩, + ⟨27, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩] + +private def g2gen2Fwd : Array (Fin 63) := #[ + ⟨10, by omega⟩, ⟨20, by omega⟩, ⟨29, by omega⟩, ⟨49, by omega⟩, ⟨55, by omega⟩, + ⟨36, by omega⟩, ⟨44, by omega⟩, ⟨14, by omega⟩, ⟨25, by omega⟩, ⟨59, by omega⟩, + ⟨40, by omega⟩, ⟨0, by omega⟩, ⟨19, by omega⟩, ⟨50, by omega⟩, ⟨35, by omega⟩, + ⟨5, by omega⟩, ⟨7, by omega⟩, ⟨47, by omega⟩, ⟨58, by omega⟩, ⟨18, by omega⟩, + ⟨24, by omega⟩, ⟨34, by omega⟩, ⟨41, by omega⟩, ⟨11, by omega⟩, ⟨17, by omega⟩, + ⟨62, by omega⟩, ⟨33, by omega⟩, ⟨6, by omega⟩, ⟨28, by omega⟩, ⟨48, by omega⟩, + ⟨45, by omega⟩, ⟨51, by omega⟩, ⟨61, by omega⟩, ⟨32, by omega⟩, ⟨42, by omega⟩, + ⟨3, by omega⟩, ⟨8, by omega⟩, ⟨22, by omega⟩, ⟨27, by omega⟩, ⟨57, by omega⟩, + ⟨46, by omega⟩, ⟨4, by omega⟩, ⟨21, by omega⟩, ⟨52, by omega⟩, ⟨31, by omega⟩, + ⟨12, by omega⟩, ⟨23, by omega⟩, ⟨53, by omega⟩, ⟨60, by omega⟩, ⟨16, by omega⟩, + ⟨26, by omega⟩, ⟨38, by omega⟩, ⟨43, by omega⟩, ⟨1, by omega⟩, ⟨9, by omega⟩, + ⟨56, by omega⟩, ⟨37, by omega⟩, ⟨2, by omega⟩, ⟨30, by omega⟩, ⟨54, by omega⟩, + ⟨39, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩] + +private def g2gen2Inv : Array (Fin 63) := #[ + ⟨11, by omega⟩, ⟨53, by omega⟩, ⟨57, by omega⟩, ⟨35, by omega⟩, ⟨41, by omega⟩, + ⟨15, by omega⟩, ⟨27, by omega⟩, ⟨16, by omega⟩, ⟨36, by omega⟩, ⟨54, by omega⟩, + ⟨0, by omega⟩, ⟨23, by omega⟩, ⟨45, by omega⟩, ⟨61, by omega⟩, ⟨7, by omega⟩, + ⟨62, by omega⟩, ⟨49, by omega⟩, ⟨24, by omega⟩, ⟨19, by omega⟩, ⟨12, by omega⟩, + ⟨1, by omega⟩, ⟨42, by omega⟩, ⟨37, by omega⟩, ⟨46, by omega⟩, ⟨20, by omega⟩, + ⟨8, by omega⟩, ⟨50, by omega⟩, ⟨38, by omega⟩, ⟨28, by omega⟩, ⟨2, by omega⟩, + ⟨58, by omega⟩, ⟨44, by omega⟩, ⟨33, by omega⟩, ⟨26, by omega⟩, ⟨21, by omega⟩, + ⟨14, by omega⟩, ⟨5, by omega⟩, ⟨56, by omega⟩, ⟨51, by omega⟩, ⟨60, by omega⟩, + ⟨10, by omega⟩, ⟨22, by omega⟩, ⟨34, by omega⟩, ⟨52, by omega⟩, ⟨6, by omega⟩, + ⟨30, by omega⟩, ⟨40, by omega⟩, ⟨17, by omega⟩, ⟨29, by omega⟩, ⟨3, by omega⟩, + ⟨13, by omega⟩, ⟨31, by omega⟩, ⟨43, by omega⟩, ⟨47, by omega⟩, ⟨59, by omega⟩, + ⟨4, by omega⟩, ⟨55, by omega⟩, ⟨39, by omega⟩, ⟨18, by omega⟩, ⟨9, by omega⟩, + ⟨48, by omega⟩, ⟨32, by omega⟩, ⟨25, by omega⟩] + +private theorem g2gen1Fwd_size : g2gen1Fwd.size = 63 := by native_decide +private theorem g2gen1Inv_size : g2gen1Inv.size = 63 := by native_decide +private theorem g2gen2Fwd_size : g2gen2Fwd.size = 63 := by native_decide +private theorem g2gen2Inv_size : g2gen2Inv.size = 63 := by native_decide + +/-- First generator of G₂(2): order 7, from companion matrix of x³ + x + 1. -/ +def g2gen1 : Equiv.Perm (Fin 63) where + toFun i := g2gen1Fwd[i.val]'(by have := g2gen1Fwd_size; omega) + invFun i := g2gen1Inv[i.val]'(by have := g2gen1Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- Second generator of G₂(2): order 6, maps vertex 0 → 10. -/ +def g2gen2 : Equiv.Perm (Fin 63) where + toFun i := g2gen2Fwd[i.val]'(by have := g2gen2Fwd_size; omega) + invFun i := g2gen2Inv[i.val]'(by have := g2gen2Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- σ₁ preserves Langer adjacency. -/ +theorem g2gen1_langer_inv : + ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen1 i) (g2gen1 j) := by + native_decide + +/-- σ₂ preserves Langer adjacency. -/ +theorem g2gen2_langer_inv : + ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen2 i) (g2gen2 j) := by + native_decide + +/-- σ₁ preserves distance-2 adjacency. -/ +theorem g2gen1_dist2_inv : + ∀ p q : Fin 63, + tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen1 p) (g2gen1 q) := by + native_decide + +/-- σ₂ preserves distance-2 adjacency. -/ +theorem g2gen2_dist2_inv : + ∀ p q : Fin 63, + tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen2 p) (g2gen2 q) := by + native_decide + +/-! ## Part 6: Word induction (structural, no native_decide) -/ + +/-- The four generator actions: σ₁, σ₁⁻¹, σ₂, σ₂⁻¹. -/ +def applyGen : Fin 4 → Equiv.Perm (Fin 63) + | 0 => g2gen1 + | 1 => g2gen1.symm + | 2 => g2gen2 + | 3 => g2gen2.symm + +/-- Apply a generator word (left-to-right). -/ +def applyWord : List (Fin 4) → Equiv.Perm (Fin 63) + | [] => Equiv.refl _ + | g :: gs => (applyGen g).trans (applyWord gs) + +private theorem symm_preserves_langer (σ : Equiv.Perm (Fin 63)) + (h : ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ i) (σ j)) + (i j : Fin 63) : + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ.symm i) (σ.symm j) := by + have := h (σ.symm i) (σ.symm j) + simp only [Equiv.apply_symm_apply] at this + exact this.symm + +private theorem applyGen_langer_inv (g : Fin 4) (i j : Fin 63) : + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (applyGen g i) (applyGen g j) := by + fin_cases g <;> simp only [applyGen] + · exact g2gen1_langer_inv i j + · exact symm_preserves_langer g2gen1 (g2gen1_langer_inv) i j + · exact g2gen2_langer_inv i j + · exact symm_preserves_langer g2gen2 (g2gen2_langer_inv) i j + +/-- Any generator word preserves Langer adjacency (structural induction). -/ +theorem applyWord_langer_inv (w : List (Fin 4)) : + ∀ i j : Fin 63, langerSimpleGraph.Adj i j ↔ + langerSimpleGraph.Adj (applyWord w i) (applyWord w j) := by + induction w with + | nil => intro i j; simp [applyWord] + | cons g gs ih => + intro i j + simp only [applyWord, Equiv.trans_apply] + rw [applyGen_langer_inv g i j] + exact ih (applyGen g i) (applyGen g j) + +private theorem symm_preserves_dist2 (σ : Equiv.Perm (Fin 63)) + (h : ∀ p q : Fin 63, tutte12Distance2Bool p q = tutte12Distance2Bool (σ p) (σ q)) + (p q : Fin 63) : + tutte12Distance2Bool p q = tutte12Distance2Bool (σ.symm p) (σ.symm q) := by + have := h (σ.symm p) (σ.symm q) + simp only [Equiv.apply_symm_apply] at this + exact this.symm + +private theorem applyGen_dist2_inv (g : Fin 4) (p q : Fin 63) : + tutte12Distance2Bool p q = tutte12Distance2Bool (applyGen g p) (applyGen g q) := by + fin_cases g <;> simp only [applyGen] + · exact g2gen1_dist2_inv p q + · exact symm_preserves_dist2 g2gen1 (g2gen1_dist2_inv) p q + · exact g2gen2_dist2_inv p q + · exact symm_preserves_dist2 g2gen2 (g2gen2_dist2_inv) p q + +/-- Any generator word preserves distance-2 adjacency (structural induction). -/ +theorem applyWord_dist2_inv (w : List (Fin 4)) : + ∀ p q : Fin 63, tutte12Distance2Bool p q = + tutte12Distance2Bool (applyWord w p) (applyWord w q) := by + induction w with + | nil => intro p q; simp [applyWord] + | cons g gs ih => + intro p q + simp only [applyWord, Equiv.trans_apply] + rw [applyGen_dist2_inv g p q] + exact ih (applyGen g p) (applyGen g q) + +/-! ## Part 7: Transitivity witnesses and main theorem -/ + +private def witnessWordData : Array (List (Fin 4)) := #[ + [], [0], [0,0,0], [0,0], [1], + [1,1,1], [1,1], [3,3,1], [3,1,2], [0,2,2,1], + [2], [3], [0,0,3,0], [1,1,3,1], [0,0,3,3], + [1,1,1,3], [1,3,0], [2,1,1], [2,1,2,0], [0,0,3,1], + [0,2], [2,1,3], [1,3,3], [3,3], [0,2,2], + [1,2,2,1], [2,0], [1,1,3], [3,0], [0,0,0,2], + [0,2,1,3], [0,3,0,2], [2,0,2,2], [2,0,2], [2,1], + [0,0,3], [3,1], [0,2,0], [1,1,3,3], [0,3,1,2], + [2,2], [1,3], [2,1,2], [0,0,3,1,1], [0,3,0], + [0,2,1], [2,2,2], [0,3,3], [2,2,1], [0,0,2], + [1,3,1], [0,2,1,1], [2,2,2,1], [0,3], [0,2,2,1,3], + [1,2], [1,2,2], [2,0,0], [0,2,2,0], [0,0,0,2,0], + [0,3,1], [3,0,0], [0,2,1,3,0]] + +private theorem witnessWordData_size : witnessWordData.size = 63 := by native_decide + +/-- BFS witness words: `witnessWord v` is a generator word mapping 0 → v. -/ +def witnessWord (v : Fin 63) : List (Fin 4) := + witnessWordData[v.val]'(by have := witnessWordData_size; omega) + +/-- Each witness word correctly maps 0 to its target vertex. -/ +theorem witnessWord_correct : + ∀ v : Fin 63, applyWord (witnessWord v) 0 = v := by + native_decide + +/-- The Langer graph and distance-2 graph agree at vertex 0. -/ +theorem graphs_agree_at_zero : + ∀ v : Fin 63, + langerSimpleGraph.Adj 0 v ↔ (tutte12Distance2Bool 0 v = true) := by + native_decide + +private theorem transport_langer (w : List (Fin 4)) (q : Fin 63) : + langerSimpleGraph.Adj (applyWord w 0) q ↔ + langerSimpleGraph.Adj 0 ((applyWord w).symm q) := by + conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q] + exact ((applyWord_langer_inv w) 0 ((applyWord w).symm q)).symm + +private theorem transport_dist2 (w : List (Fin 4)) (q : Fin 63) : + tutte12Distance2Bool (applyWord w 0) q = + tutte12Distance2Bool 0 ((applyWord w).symm q) := by + conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q] + exact ((applyWord_dist2_inv w) 0 ((applyWord w).symm q)).symm + +/-- **The Langer graph equals the distance-2 graph of the Tutte 12-cage +restricted to points** — proved structurally via G₂(2) transitivity. + +The argument: +1. Let σ = applyWord (witnessWord p), so σ(0) = p +2. Adj p q ↔ Adj 0 (σ⁻¹ q) [by transport_langer] +3. dist2 p q = dist2 0 (σ⁻¹ q) [by transport_dist2] +4. Adj 0 (σ⁻¹ q) ↔ dist2 0 (σ⁻¹ q) [by graphs_agree_at_zero] -/ +theorem langer_eq_tutte12_distance2' : + ∀ p q : Fin 63, + langerSimpleGraph.Adj p q ↔ (tutte12Distance2Bool p q = true) := by + intro p q + rw [← witnessWord_correct p] + rw [transport_langer, transport_dist2] + exact graphs_agree_at_zero _ + +/-! ## The Langer graph is a Sabidussi coset graph + +G₂(2) = ⟨σ₁, σ₂⟩ acts vertex-transitively on the 63 points of GH(2,2), +so by the Sabidussi representation theorem: + `langerSimpleGraph ≃g cosetGraph(Stab_G₂(0), connectionSet G₂ langer 0)` -/ + +/-- The two G₂(2) generators as a `Fin 2`-indexed family. -/ +def langerGens : Fin 2 → Equiv.Perm (Fin 63) + | 0 => g2gen1 + | 1 => g2gen2 + +/-- G₂(2) as a subgroup of Sym(63), generated by σ₁ and σ₂. -/ +def langerG : Subgroup (Equiv.Perm (Fin 63)) := + Subgroup.closure (Set.range langerGens) + +private theorem applyGen_mem (i : Fin 4) : applyGen i ∈ langerG := by + unfold langerG + match i with + | 0 => exact Subgroup.subset_closure ⟨0, rfl⟩ + | 1 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨0, rfl⟩) + | 2 => exact Subgroup.subset_closure ⟨1, rfl⟩ + | 3 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨1, rfl⟩) + +private theorem applyWord_mem (w : List (Fin 4)) : applyWord w ∈ langerG := by + induction w with + | nil => exact Subgroup.one_mem _ + | cons i rest ih => exact langerG.mul_mem ih (applyGen_mem i) + +noncomputable instance langerMulAction : MulAction langerG (Fin 63) := + MulAction.compHom (Fin 63) langerG.subtype + +noncomputable instance langerGraphAction : + GraphAction langerG (Fin 63) langerSimpleGraph where + adj_smul := by + intro ⟨σ, hσ⟩ u v hadj + change langerSimpleGraph.Adj (σ u) (σ v) + revert u v; change ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v) + refine Subgroup.closure_induction + (p := fun σ _ => ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v)) + ?_ ?_ ?_ ?_ hσ + · intro x ⟨i, hi⟩; subst hi + match i with + | 0 => exact fun u v h => (g2gen1_langer_inv u v).mp h + | 1 => exact fun u v h => (g2gen2_langer_inv u v).mp h + · intro u v h; simpa + · intro x y _ _ hx hy u v hadj + simp only [Equiv.Perm.mul_apply]; exact hx _ _ (hy u v hadj) + · intro x _ hx u v hadj + let f : { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } → + { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } := + fun ⟨⟨a, b⟩, hab⟩ => ⟨⟨x a, x b⟩, hx a b hab⟩ + have hf_surj : Function.Surjective f := Finite.surjective_of_injective (by + intro ⟨⟨a₁, b₁⟩, _⟩ ⟨⟨a₂, b₂⟩, _⟩ h + simp only [f, Subtype.mk.injEq, Prod.mk.injEq] at h + exact Subtype.ext (Prod.ext (x.injective h.1) (x.injective h.2))) + obtain ⟨⟨⟨a, b⟩, hab⟩, heq⟩ := hf_surj ⟨⟨u, v⟩, hadj⟩ + 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 + +noncomputable instance langerPretransitive : + MulAction.IsPretransitive langerG (Fin 63) where + exists_smul_eq := by + intro x y + let σ_x := applyWord (witnessWord x) + let σ_y := applyWord (witnessWord y) + have hmem : σ_x.symm.trans σ_y ∈ langerG := + langerG.mul_mem (applyWord_mem _) (langerG.inv_mem (applyWord_mem _)) + exact ⟨⟨σ_x.symm.trans σ_y, hmem⟩, by + change (σ_x.symm.trans σ_y) x = y + simp only [Equiv.trans_apply] + rw [show σ_x.symm x = 0 from by + rw [Equiv.symm_apply_eq]; exact (witnessWord_correct x).symm] + exact witnessWord_correct y⟩ + +/-- **The Langer graph is a Sabidussi coset graph.** + + `langerSimpleGraph ≃g Sab(G₂(2), H₁₉₂, D)` + +where H₁₉₂ = Stab(0) has order 192. -/ +noncomputable def langerSabidussiIso : + langerSimpleGraph ≃g SimpleGraph.cosetGraph + (MulAction.stabilizer langerG (0 : Fin 63)) + (connectionSet langerG langerSimpleGraph 0) + (connectionSet.isConnectionSet 0) := + sabidussiIso 0 + +/-! ## Primitivity of the G₂(2) action + +The action of G₂(2) on the 63 points of GH(2,2) is **primitive**: the point +stabiliser H₁₉₂ (order 192 = 12096/63) is a maximal subgroup of G₂(2). + +We verify this directly using Atkinson's algorithm (1975): for each v ≠ 0, +compute the smallest block containing {0, v} by propagating equivalences +through generators. A block B satisfies: ∀ g ∈ G, gB = B ∨ gB ∩ B = ∅. +Equivalently: if i ~ j (same block) then g(i) ~ g(j). Starting from +0 ~ v, we propagate via a queue of newly-merged pairs until stable. If +the block is always all of Ω, no non-trivial block system exists. + +The queue-based approach processes only the O(n) actual merges rather +than scanning all elements at each round, keeping the computation +small. -/ + +/-- All four generator permutations: σ₁, σ₁⁻¹, σ₂, σ₂⁻¹. -/ +private def g2AllGens : List (Equiv.Perm (Fin 63)) := + [g2gen1, g2gen1.symm, g2gen2, g2gen2.symm] + +/-- Merge two equivalence classes: replace all occurrences of `hi` + with `lo`. -/ +private def mergeRep (f : Fin 63 → Fin 63) (lo hi : Fin 63) : + Fin 63 → Fin 63 := + fun i => let fi := f i; if fi = hi then lo else fi + +/-- Atkinson's algorithm: compute the smallest block containing + {0, v}. + + State: `(queue, partition)` where `queue` is a list of + newly-merged pairs and `partition : Fin 63 → Fin 63` maps each + element to its class representative. + + At each step, pop a pair (x, y) from the queue. For each + generator g, check if g(x) and g(y) have the same + representative. If not, merge their classes and enqueue the + new pair. Terminate when the queue is empty. + + `fuel` bounds the number of steps (at most 62 merges × + 4 generators = 248 enqueued pairs, so fuel = 300 is + generous). -/ +private def atkinson (gens : List (Equiv.Perm (Fin 63))) + (queue : List (Fin 63 × Fin 63)) + (part : Fin 63 → Fin 63) : + Nat → Fin 63 → Fin 63 + | 0 => part + | fuel + 1 => + match queue with + | [] => part + | (x, y) :: rest => + let Acc := + List (Fin 63 × Fin 63) × (Fin 63 → Fin 63) + let (newPairs, part') := + gens.foldl (fun (acc : Acc) g => + let (pairs, p) := acc + let rgx := p (g x) + let rgy := p (g y) + if rgx = rgy then (pairs, p) + else + let lo := min rgx rgy + let hi := max rgx rgy + ((lo, hi) :: pairs, mergeRep p lo hi)) + ([], part) + atkinson gens (rest ++ newPairs) part' fuel + +/-- Check that Atkinson's algorithm starting from {0, v} merges + all vertices into a single class (representative 0). -/ +private def blockIsFullBool (v : Fin 63) : Bool := + let initPart : Fin 63 → Fin 63 := fun i => + if i = v then 0 else i + let finalPart := + atkinson g2AllGens [(0, v)] initPart 300 + decide (∀ w : Fin 63, finalPart w = 0) + +/-- **Primitivity of the G₂(2) action on the 63 points of GH(2,2).** + +For every vertex v ≠ 0, Atkinson's algorithm starting from 0 ~ v +merges all 63 vertices into a single equivalence class. This means +no non-trivial block system exists, so the point stabiliser +H₁₉₂ ≤ G₂(2) is a **maximal subgroup** — there is no subgroup K +with H₁₉₂ < K < G₂(2). + +The Langer graph is primitive, and unlike Zhou-6 (the Z₂ quotient of +the cubic Zhou graph F182A) it admits no cubic double cover +(see `tutte12_points_independent` below). -/ +theorem langer_action_primitive : + ∀ v : Fin 63, v ≠ 0 → + blockIsFullBool v = true := by + native_decide + +/-! ## No cubic double cover of the Langer graph + +The Zhou graph (F182A, 182 vertices, cubic) is a Z₂ double cover of its +quotient Zhou-6 (91 vertices, 6-regular) via the block system S₃ < D₁₂. +One might ask: does the same hold for the Langer graph? That is, does +there exist a 126-vertex cubic graph covering the Langer graph via a +2:1 map? + +The natural candidate is the Tutte 12-cage (126 vertices, cubic, same +G₂(2) symmetry). However, it **cannot** cover the Langer graph: + +1. The Tutte 12-cage is semisymmetric (not vertex-transitive), while + any covering of the vertex-transitive Langer graph must be + vertex-transitive. + +2. More fundamentally, the point stabiliser H₁₉₂ in G₂(2) has three + index-2 subgroups of order 96, but **none** yield a size-3 + suborbit in the coset action on 126 points. The smallest suborbits + are size 6 and 12 — no cubic Sabidussi graph exists. + +Verification: the Tutte 12-cage point subgraph (induced on vertices +0–62) has no edges, so no point-point edge can cover a Langer edge. +-/ + +/-- The Tutte 12-cage has no edges between points: the induced + subgraph on vertices 0–62 is edgeless. This obstructs any + covering map to the Langer graph, which has 189 edges between + its 63 vertices. -/ +theorem tutte12_points_independent : + ∀ p q : Fin 63, + ¬tutte12CageGraph.Adj + ⟨p.val, by omega⟩ ⟨q.val, by omega⟩ := by + native_decide + +/-! ## Zhou-6: PSL(2,13) acts primitively on 91 points + +The **Zhou-6 graph** (91 vertices, 6-regular) is Sab(PSL(2,13), D₁₂). +The stabiliser D₁₂ is maximal in PSL(2,13), so the action is primitive. +We verify this with the same Atkinson algorithm used for the Langer +graph. -/ + +private def zhou6Gen1Fwd : Array (Fin 91) := #[ + 1, 3, 5, 7, 8, 10, 12, 13, 15, 17, 18, 20, 6, 21, 23, 25, 27, 26, + 30, 32, 34, 0, 37, 39, 41, 42, 44, 16, 47, 48, 49, 51, 53, 31, 24, + 55, 56, 58, 60, 61, 62, 46, 65, 64, 57, 69, 11, 40, 66, 2, 71, 73, + 75, 76, 77, 79, 38, 70, 81, 82, 59, 83, 54, 85, 45, 4, 35, 63, 43, + 86, 9, 33, 22, 50, 87, 84, 88, 28, 14, 29, 19, 89, 36, 78, 52, 74, + 68, 90, 80, 72, 67] +private def zhou6Gen1Inv : Array (Fin 91) := #[ + 21, 0, 49, 1, 65, 2, 12, 3, 4, 70, 5, 46, 6, 7, 78, 8, 27, 9, 10, + 80, 11, 13, 72, 14, 34, 15, 17, 16, 77, 79, 18, 33, 19, 71, 20, 66, + 82, 22, 56, 23, 47, 24, 25, 68, 26, 64, 41, 28, 29, 30, 73, 31, 84, + 32, 62, 35, 36, 44, 37, 60, 38, 39, 40, 67, 43, 42, 48, 90, 86, 45, + 57, 50, 89, 51, 85, 52, 53, 54, 83, 55, 88, 58, 59, 61, 75, 63, 69, + 74, 76, 81, 87] +private def zhou6Gen2Fwd : Array (Fin 91) := #[ + 2, 4, 6, 5, 9, 11, 0, 14, 16, 1, 19, 3, 17, 22, 24, 26, 28, 29, + 31, 33, 35, 36, 38, 40, 7, 43, 45, 46, 8, 12, 50, 52, 54, 10, 55, + 53, 57, 59, 13, 51, 63, 64, 66, 67, 68, 15, 70, 56, 47, 41, 72, 74, + 18, 20, 78, 80, 48, 21, 58, 69, 44, 73, 84, 23, 49, 79, 71, 25, 60, + 37, 27, 42, 30, 81, 39, 85, 76, 65, 32, 77, 34, 61, 86, 62, 83, 89, + 90, 87, 88, 75, 82] +private def zhou6Gen2Inv : Array (Fin 91) := #[ + 6, 9, 0, 11, 1, 3, 2, 24, 28, 4, 33, 5, 29, 38, 7, 45, 8, 12, 52, + 10, 53, 57, 13, 63, 14, 67, 15, 70, 16, 17, 72, 18, 78, 19, 80, 20, + 21, 69, 22, 74, 23, 49, 71, 25, 60, 26, 27, 48, 56, 64, 30, 39, 31, + 35, 32, 34, 47, 36, 58, 37, 68, 81, 83, 40, 41, 77, 42, 43, 44, 59, + 46, 66, 50, 61, 51, 89, 76, 79, 54, 65, 55, 73, 90, 84, 62, 75, 82, + 87, 88, 85, 86] + +private theorem zhou6Gen1Fwd_size : zhou6Gen1Fwd.size = 91 := by + native_decide +private theorem zhou6Gen1Inv_size : zhou6Gen1Inv.size = 91 := by + native_decide +private theorem zhou6Gen2Fwd_size : zhou6Gen2Fwd.size = 91 := by + native_decide +private theorem zhou6Gen2Inv_size : zhou6Gen2Inv.size = 91 := by + native_decide + +/-- First generator of PSL(2,13) on 91 cosets of D₁₂. -/ +private def zhou6Gen1 : Equiv.Perm (Fin 91) where + toFun i := zhou6Gen1Fwd[i.val]'(by + have := zhou6Gen1Fwd_size; omega) + invFun i := zhou6Gen1Inv[i.val]'(by + have := zhou6Gen1Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- Second generator of PSL(2,13) on 91 cosets of D₁₂. -/ +private def zhou6Gen2 : Equiv.Perm (Fin 91) where + toFun i := zhou6Gen2Fwd[i.val]'(by + have := zhou6Gen2Fwd_size; omega) + invFun i := zhou6Gen2Inv[i.val]'(by + have := zhou6Gen2Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +private def zhou6AllGens : List (Equiv.Perm (Fin 91)) := + [zhou6Gen1, zhou6Gen1.symm, zhou6Gen2, zhou6Gen2.symm] + +private def mergeRep91 (f : Fin 91 → Fin 91) (lo hi : Fin 91) : + Fin 91 → Fin 91 := + fun i => let fi := f i; if fi = hi then lo else fi + +private def atkinson91 (gens : List (Equiv.Perm (Fin 91))) + (queue : List (Fin 91 × Fin 91)) + (part : Fin 91 → Fin 91) : + Nat → Fin 91 → Fin 91 + | 0 => part + | fuel + 1 => + match queue with + | [] => part + | (x, y) :: rest => + let Acc := + List (Fin 91 × Fin 91) × (Fin 91 → Fin 91) + let (newPairs, part') := + gens.foldl (fun (acc : Acc) g => + let (pairs, p) := acc + let rgx := p (g x) + let rgy := p (g y) + if rgx = rgy then (pairs, p) + else + let lo := min rgx rgy + let hi := max rgx rgy + ((lo, hi) :: pairs, mergeRep91 p lo hi)) + ([], part) + atkinson91 gens (rest ++ newPairs) part' fuel + +private def zhou6BlockIsFullBool (v : Fin 91) : Bool := + let initPart : Fin 91 → Fin 91 := fun i => + if i = v then 0 else i + let finalPart := + atkinson91 zhou6AllGens [(0, v)] initPart 400 + decide (∀ w : Fin 91, finalPart w = 0) + +/-- **Primitivity of the PSL(2,13) action on 91 points.** + +For every vertex v ≠ 0, Atkinson's algorithm starting from 0 ~ v +merges all 91 vertices into a single equivalence class. The point +stabiliser D₁₂ ≤ PSL(2,13) is a maximal subgroup. + +The Zhou-6 graph Sab(PSL(2,13), D₁₂) is primitive and admits a +cubic double cover: the Zhou graph F182A = Sab(PSL(2,13), S₃) +covers it via S₃ ≤ D₁₂. -/ +theorem zhou6_action_primitive : + ∀ v : Fin 91, v ≠ 0 → + zhou6BlockIsFullBool v = true := by + native_decide 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..caebcd8cfdedfe --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean @@ -0,0 +1,173 @@ +/- +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 + +/-! ## Coset projection + +When `H ≤ K`, the natural projection `G ⧸ H → G ⧸ K` sends `gH ↦ gK`. +If `D` is a connection set for both `H` and `K`, this projection is a +graph homomorphism: adjacency in `Sab(G, H, D)` implies adjacency in +`Sab(G, K, D)`. + +This is the Sabidussi analogue of quotient by a block system: the orbits +of `K` on `G ⧸ H` form a system of blocks of size `[K : H]`, and the +quotient graph is `Sab(G, K, D)`. -/ + +/-- The natural projection `G ⧸ H → G ⧸ K` when `H ≤ K`. -/ +def cosetProjection (H K : Subgroup G) (hle : H ≤ K) : + G ⧸ H → G ⧸ K := + Quotient.map id fun _ _ hab => by + change (QuotientGroup.leftRel K).r _ _ + have hab' : (QuotientGroup.leftRel H).r _ _ := hab + rw [QuotientGroup.leftRel_apply] at hab' ⊢ + exact hle hab' + +@[simp] +theorem cosetProjection_mk (H K : Subgroup G) (hle : H ≤ K) + (g : G) : cosetProjection H K hle ⟦g⟧ = ⟦g⟧ := + rfl + +/-- **Coset projection is a graph homomorphism**: if `H ≤ K` and `D` is a + connection set for both, then adjacency in `Sab(G, H, D)` implies + adjacency in `Sab(G, K, D)`. + + The proof is trivial: adjacency is `x⁻¹y ∈ D` in both graphs. + The subgroup only determines the coset equivalence, not the adjacency test. -/ +theorem SimpleGraph.cosetGraph.proj_adj + {H K : Subgroup G} (hle : H ≤ K) {D : Set G} + (hDH : IsConnectionSet H D) (hDK : IsConnectionSet K D) + (q₁ q₂ : G ⧸ H) : + (cosetGraph H D hDH).Adj q₁ q₂ → + (cosetGraph K D hDK).Adj (cosetProjection H K hle q₁) + (cosetProjection H K hle q₂) := + Quotient.inductionOn₂ q₁ q₂ fun _ _ h => h + +/-- The coset projection is surjective. -/ +theorem cosetProjection_surjective (H K : Subgroup G) (hle : H ≤ K) : + Function.Surjective (cosetProjection H K hle) := + fun q => Quotient.inductionOn q fun g => ⟨⟦g⟧, rfl⟩ 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)