fix: filenames with typos in doc (#5836)

Mathlib/LinearAlgebra/Span.lean

@@ -296,7 +296,7 @@ theorem subset_span_trans {U V W : Set M} (hUV : U ⊆ Submodule.span R V)
   (Submodule.gi R M).gc.le_u_l_trans hUV hVW
 #align submodule.subset_span_trans Submodule.subset_span_trans
 
-/-- See `submodule.span_smul_eq` (in `ring_theory.ideal.operations`) for
+/-- See `submodule.span_smul_eq` (in `RingTheory.Ideal.Operations`) for
 `span R (r • s) = r • span R s` that holds for arbitrary `r` in a `CommSemiring`. -/
 theorem span_smul_eq_of_isUnit (s : Set M) (r : R) (hr : IsUnit r) : span R (r • s) = span R s := by
   apply le_antisymm

Mathlib/NumberTheory/Pell.lean

@@ -20,7 +20,7 @@ import Mathlib.NumberTheory.Zsqrtd.Basic
 that is not a square, and one is interested in solutions in integers $x$ and $y$.
 
 In this file, we aim at providing all of the essential theory of Pell's Equation for general $d$
-(as opposed to the contents of `number_theory.pell_matiyasevic`, which is specific to the case
+(as opposed to the contents of `NumberTheory.PellMatiyasevic`, which is specific to the case
 $d = a^2 - 1$ for some $a > 1$).
 
 We begin by defining a type `Pell.Solution₁ d` for solutions of the equation,

Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

@@ -26,7 +26,7 @@ The homomorphism `GaussianInt.toComplex` into the complex numbers is also define
 
 ## See also
 
-See `number_theory.zsqrtd.gaussian_int` for:
+See `NumberTheory.Zsqrtd.QuadraticReciprocity` for:
 * `prime_iff_mod_four_eq_three_of_nat_prime`:
   A prime natural number is prime in `ℤ[i]` if and only if it is `3` mod `4`
 

Mathlib/RingTheory/Derivation/Basic.lean

@@ -22,10 +22,10 @@ This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `
 - `Derivation.llcomp`: We may compose linear maps and derivations to obtain a derivation,
   and the composition is bilinear.
 
-See `ring_theory.derivation.lie` for
+See `RingTheory.Derivation.Lie` for
 - `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form a lie algebra over `R`.
 
-and `ring_theory.derivation.to_square_zero` for
+and `RingTheory.Derivation.ToSquareZero` for
 - `derivation_to_square_zero_equiv_lift`: The `R`-derivations from `A` into a square-zero ideal `I`
   of `B` corresponds to the lifts `A →ₐ[R] B` of the map `A →ₐ[R] B ⧸ I`.
 

Mathlib/RingTheory/Ideal/Over.lean

@@ -99,7 +99,7 @@ theorem injective_quotient_le_comap_map (P : Ideal R[X]) :
 R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))
 ```
 commutes.  It is used, for instance, in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`,
-in the file `ring_theory/jacobson`.
+in the file `RingTheory.Jacobson`.
 -/
 theorem quotient_mk_maps_eq (P : Ideal R[X]) :
     ((Quotient.mk (map (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)).comp C).comp

Mathlib/RingTheory/Localization/AtPrime.lean

@@ -27,7 +27,7 @@ import Mathlib.RingTheory.Localization.Ideal
 
 ## Implementation notes
 
-See `src/ring_theory/Localization/basic.lean` for a design overview.
+See `RingTheory.Localization.Basic` for a design overview.
 
 ## Tags
 localization, ring localization, commutative ring localization, characteristic predicate,

Mathlib/RingTheory/Nakayama.lean

@@ -32,7 +32,7 @@ This file contains some alternative statements of Nakayama's Lemma as found in
 
 Note that a version of Statement (1) in
 [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV) can be found in
-`ring_theory/noetherian` under the name
+`RingTheory.Noetherian` under the name
 `Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul`
 
 ## References

Mathlib/RingTheory/WittVector/Defs.lean

@@ -14,13 +14,13 @@ import Mathlib.RingTheory.WittVector.StructurePolynomial
 # Witt vectors
 
 In this file we define the type of `p`-typical Witt vectors and ring operations on it.
-The ring axioms are verified in `ring_theory/witt_vector/basic.lean`.
+The ring axioms are verified in `RingTheory.WittVector.Basic`.
 
 For a fixed commutative ring `R` and prime `p`,
 a Witt vector `x : 𝕎 R` is an infinite sequence `ℕ → R` of elements of `R`.
 However, the ring operations `+` and `*` are not defined in the obvious component-wise way.
 Instead, these operations are defined via certain polynomials
-using the machinery in `structure_polynomial.lean`.
+using the machinery in `StructurePolynomial.lean`.
 The `n`th value of the sum of two Witt vectors can depend on the `0`-th through `n`th values
 of the summands. This effectively simulates a “carrying” operation.
 

Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

@@ -28,7 +28,7 @@ The construction proceeds by recursively defining a sequence of coefficients as
 polynomial equation in `k`. We must define these as generic polynomials using Witt vector API
 (`WittVector.wittMul`, `wittPolynomial`) to show that they satisfy the desired equation.
 
-Preliminary work is done in the dependency `ring_theory.witt_vector.mul_coeff`
+Preliminary work is done in the dependency `RingTheory.WittVector.MulCoeff`
 to isolate the `n+1`st coefficients of `x` and `y` in the `n+1`st coefficient of `x*y`.
 
 This construction is described in Dupuis, Lewis, and Macbeth,

Mathlib/Topology/Category/TopCat/Limits/Konig.lean

@@ -28,7 +28,7 @@ This also applies to inverse limits, where `{J : Type u} [preorder J] [is_direct
 
 The theorem is specialized to nonempty finite types (which are compact Hausdorff with the
 discrete topology) in lemmas `nonempty_sections_of_finite_cofiltered_system` and
-`nonempty_sections_of_finite_inverse_system` in the file `category_theory.cofiltered_system`.
+`nonempty_sections_of_finite_inverse_system` in the file `CategoryTheory.CofilteredSystem`.
 
 (See <https://stacks.math.columbia.edu/tag/086J> for the Set version.)
 -/