doc: capitalize cartesian (leanprover-community#29294)

Cartesian is derived from the name of a mathematician, which means it is capitalized in English. The only real deviation from this pattern I know of is "abelian".

Author: harahu

Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

@@ -18,7 +18,7 @@ and sums indexed by finite sets.
 ## Main declarations
 
 * `Multiset.prod`: `s.prod f` is the product of `f i` over all `i ∈ s`. Not to be mistaken with
-  the cartesian product `Multiset.product`.
+  the Cartesian product `Multiset.product`.
 * `Multiset.sum`: `s.sum f` is the sum of `f i` over all `i ∈ s`.
 -/
 

Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean

@@ -17,7 +17,7 @@ and sums indexed by finite sets.
 ## Main declarations
 
 * `Multiset.prod`: `s.prod f` is the product of `f i` over all `i ∈ s`. Not to be mistaken with
-  the cartesian product `Multiset.product`.
+  the Cartesian product `Multiset.product`.
 * `Multiset.sum`: `s.sum f` is the sum of `f i` over all `i ∈ s`.
 -/
 

Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean

@@ -7,9 +7,9 @@ import Mathlib.Algebra.Category.CommAlgCat.Basic
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 
 /-!
-# The cocartesian monoidal category structure on commutative `R`-algebras
+# The co-Cartesian monoidal category structure on commutative `R`-algebras
 
-This file provides the cocartesian-monoidal category structure on `CommAlgCat R` constructed
+This file provides the co-Cartesian-monoidal category structure on `CommAlgCat R` constructed
 explicitly using the tensor product.
 -/
 

Mathlib/Algebra/Category/Grp/Biproducts.lean

@@ -51,7 +51,7 @@ theorem binaryProductLimitCone_cone_π_app_right (G H : AddCommGrp.{u}) :
   rfl
 
 /-- We verify that the biproduct in `AddCommGrp` is isomorphic to
-the cartesian product of the underlying types:
+the Cartesian product of the underlying types:
 -/
 noncomputable def biprodIsoProd (G H : AddCommGrp.{u}) :
     (G ⊞ H : AddCommGrp) ≅ AddCommGrp.of (G × H) :=
@@ -72,7 +72,7 @@ namespace HasLimit
 variable {J : Type w} (f : J → AddCommGrp.{max w u})
 
 /-- The map from an arbitrary cone over an indexed family of abelian groups
-to the cartesian product of those groups.
+to the Cartesian product of those groups.
 -/
 @[simps!]
 def lift (s : Fan f) : s.pt ⟶ AddCommGrp.of (∀ j, f j) :=

Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

@@ -63,7 +63,7 @@ theorem binaryProductLimitCone_cone_π_app_right (M N : ModuleCat.{v} R) :
   rfl
 
 /-- We verify that the biproduct in `ModuleCat R` is isomorphic to
-the cartesian product of the underlying types:
+the Cartesian product of the underlying types:
 -/
 noncomputable def biprodIsoProd (M N : ModuleCat.{v} R) :
     (M ⊞ N : ModuleCat.{v} R) ≅ ModuleCat.of R (M × N) :=
@@ -84,7 +84,7 @@ namespace HasLimit
 variable {J : Type w} (f : J → ModuleCat.{max w v} R)
 
 /-- The map from an arbitrary cone over an indexed family of abelian groups
-to the cartesian product of those groups.
+to the Cartesian product of those groups.
 -/
 @[simps!]
 def lift (s : Fan f) : s.pt ⟶ ModuleCat.of R (∀ j, f j) :=

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -20,7 +20,7 @@ In this file we provide the explicit (co)cones for various (co)limits in `CommRi
 * tensor product over `ℤ` is the binary coproduct
 * `ℤ` is the initial object
 * `0` is the strict terminal object
-* cartesian product is the product
+* Cartesian product is the product
 * arbitrary direct product of a family of rings is the product object (Pi object)
 * `RingHom.eqLocus` is the equalizer
 
@@ -257,12 +257,12 @@ section Product
 
 variable (A B : CommRingCat.{u})
 
-/-- The product in `CommRingCat` is the cartesian product. This is the binary fan. -/
+/-- The product in `CommRingCat` is the Cartesian product. This is the binary fan. -/
 @[simps! pt]
 def prodFan : BinaryFan A B :=
   BinaryFan.mk (CommRingCat.ofHom <| RingHom.fst A B) (CommRingCat.ofHom <| RingHom.snd A B)
 
-/-- The product in `CommRingCat` is the cartesian product. -/
+/-- The product in `CommRingCat` is the Cartesian product. -/
 def prodFanIsLimit : IsLimit (prodFan A B) where
   lift c := ofHom <| RingHom.prod (c.π.app ⟨WalkingPair.left⟩).hom (c.π.app ⟨WalkingPair.right⟩).hom
   fac c j := by
@@ -286,14 +286,14 @@ section Pi
 variable {ι : Type u} (R : ι → CommRingCat.{u})
 
 /--
-The categorical product of rings is the cartesian product of rings. This is its `Fan`.
+The categorical product of rings is the Cartesian product of rings. This is its `Fan`.
 -/
 @[simps! pt]
 def piFan : Fan R :=
   Fan.mk (CommRingCat.of ((i : ι) → R i)) (fun i ↦ ofHom <| Pi.evalRingHom _ i)
 
 /--
-The categorical product of rings is the cartesian product of rings.
+The categorical product of rings is the Cartesian product of rings.
 -/
 def piFanIsLimit : IsLimit (piFan R) where
   lift s := ofHom <| Pi.ringHom fun i ↦ (s.π.1 ⟨i⟩).hom

Mathlib/Algebra/Ring/Fin.lean

@@ -13,12 +13,12 @@ This file collects some basic results involving rings and the `Fin` type
 
 ## Main results
 
-* `RingEquiv.piFinTwo`: The product over `Fin 2` of some rings is the cartesian product
+* `RingEquiv.piFinTwo`: The product over `Fin 2` of some rings is the Cartesian product
 
 -/
 
 
-/-- The product over `Fin 2` of some rings is just the cartesian product of these rings. -/
+/-- The product over `Fin 2` of some rings is just the Cartesian product of these rings. -/
 @[simps]
 def RingEquiv.piFinTwo (R : Fin 2 → Type*) [∀ i, Semiring (R i)] :
     (∀ i : Fin 2, R i) ≃+* R 0 × R 1 :=

Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

@@ -16,7 +16,7 @@ We show that this class is stable under composition and base change.
 
 We also show that (`AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback`)
 if `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of
-`X × Y` (cartesian product as topological spaces) with the induced topology.
+`X × Y` (Cartesian product as topological spaces) with the induced topology.
 -/
 
 open CategoryTheory CategoryTheory.Limits Topology
@@ -99,7 +99,7 @@ lemma mono_of_injective [SurjectiveOnStalks f] (hf : Function.Injective f.base)
   · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)
 
 /-- If `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of
-`X × Y` (cartesian product as topological spaces) with the induced topology. -/
+`X × Y` (Cartesian product as topological spaces) with the induced topology. -/
 lemma isEmbedding_pullback {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) [SurjectiveOnStalks g] :
     IsEmbedding (fun x ↦ ((pullback.fst f g).base x, (pullback.snd f g).base x)) := by
   let L := (fun x ↦ ((pullback.fst f g).base x, (pullback.snd f g).base x))

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -501,8 +501,8 @@ end linear
 /-! ### The Cartesian product of two C^n functions is C^n. -/
 section prod
 
-/-- If two functions `f` and `g` admit Taylor series `p` and `q` in a set `s`, then the cartesian
-product of `f` and `g` admits the cartesian product of `p` and `q` as a Taylor series. -/
+/-- If two functions `f` and `g` admit Taylor series `p` and `q` in a set `s`, then the Cartesian
+product of `f` and `g` admits the Cartesian product of `p` and `q` as a Taylor series. -/
 theorem HasFTaylorSeriesUpToOn.prodMk {n : WithTop ℕ∞}
     (hf : HasFTaylorSeriesUpToOn n f p s) {g : E → G}
     {q : E → FormalMultilinearSeries 𝕜 E G} (hg : HasFTaylorSeriesUpToOn n g q s) :
@@ -519,7 +519,7 @@ theorem HasFTaylorSeriesUpToOn.prodMk {n : WithTop ℕ∞}
 @[deprecated (since := "2025-03-09")]
 alias HasFTaylorSeriesUpToOn.prod := HasFTaylorSeriesUpToOn.prodMk
 
-/-- The cartesian product of `C^n` functions at a point in a domain is `C^n`. -/
+/-- The Cartesian product of `C^n` functions at a point in a domain is `C^n`. -/
 @[fun_prop]
 theorem ContDiffWithinAt.prodMk {s : Set E} {f : E → F} {g : E → G}
     (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
@@ -543,7 +543,7 @@ theorem ContDiffWithinAt.prodMk {s : Set E} {f : E → F} {g : E → G}
 @[deprecated (since := "2025-03-09")]
 alias ContDiffWithinAt.prod := ContDiffWithinAt.prodMk
 
-/-- The cartesian product of `C^n` functions on domains is `C^n`. -/
+/-- The Cartesian product of `C^n` functions on domains is `C^n`. -/
 @[fun_prop]
 theorem ContDiffOn.prodMk {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffOn 𝕜 n f s)
     (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x : E => (f x, g x)) s := fun x hx =>
@@ -552,7 +552,7 @@ theorem ContDiffOn.prodMk {s : Set E} {f : E → F} {g : E → G} (hf : ContDiff
 @[deprecated (since := "2025-03-09")]
 alias ContDiffOn.prod := ContDiffOn.prodMk
 
-/-- The cartesian product of `C^n` functions at a point is `C^n`. -/
+/-- The Cartesian product of `C^n` functions at a point is `C^n`. -/
 @[fun_prop]
 theorem ContDiffAt.prodMk {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x)
     (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x : E => (f x, g x)) x :=
@@ -561,7 +561,7 @@ theorem ContDiffAt.prodMk {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f
 @[deprecated (since := "2025-03-09")]
 alias ContDiffAt.prod := ContDiffAt.prodMk
 
-/-- The cartesian product of `C^n` functions is `C^n`. -/
+/-- The Cartesian product of `C^n` functions is `C^n`. -/
 @[fun_prop]
 theorem ContDiff.prodMk {f : E → F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
     ContDiff 𝕜 n fun x : E => (f x, g x) :=

Mathlib/Analysis/Calculus/Deriv/Prod.lean

@@ -30,7 +30,7 @@ variable {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {s : Set 𝕜} {L : Filter 
 
 section CartesianProduct
 
-/-! ### Derivative of the cartesian product of two functions -/
+/-! ### Derivative of the Cartesian product of two functions -/
 
 
 variable {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G]