Fix a few lean3 names.

leanprover-community · Jul 22, 2024 · e0ccbbe · e0ccbbe
1 parent 9228d9b
commit e0ccbbe
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
@@ -230,7 +230,7 @@ variable {𝕜 : Type*} [RCLike 𝕜]
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
 
--- variant of `orthogonal_projection_singleton`
+-- variant of `orthogonalProjection_singleton`
 theorem orthogonalProjection_singleton' {v : E} :
     (𝕜 ∙ v).subtypeL.comp (orthogonalProjection (𝕜 ∙ v)) =
       (1 / (‖v‖ : 𝕜) ^ 2) • .toSpanSingleton 𝕜 v ∘L InnerProductSpace.toDual 𝕜 E v := by

diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -103,7 +103,7 @@ theorem reallyConvexHull_mono : Monotone (reallyConvexHull 𝕜 : Set E → Set
   rintro s t h _ ⟨w, w_pos, supp_w, sum_w, rfl⟩
   exact ⟨w, w_pos, supp_w.trans h, sum_w, rfl⟩
 
-/-- Generalization of `convex` to semirings. We only add the `s = ∅` clause if `𝕜` is trivial. -/
+/-- Generalization of `Convex` to semirings. We only add the `s = ∅` clause if `𝕜` is trivial. -/
 def ReallyConvex (𝕜 : Type*) {E : Type*} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E]
     (s : Set E) : Prop :=
   s = ∅ ∨ ∀ w : E → 𝕜, 0 ≤ w → support w ⊆ s → ∑ᶠ x, w x = 1 → ∑ᶠ x, w x • x ∈ s

diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
@@ -71,7 +71,7 @@ theorem inner_crossProduct_apply_apply_self (u : E) (v : (ℝ ∙ u)ᗮ) : ⟪u
   rw [ω.inner_crossProduct_apply u v v]
   exact ω.volumeForm.map_eq_zero_of_eq ![u, v, v] (by simp) (by norm_num; decide : (1 : Fin 3) ≠ 2)
 
-/-- The map `cross_product`, upgraded from linear to continuous-linear; useful for calculus. -/
+/-- The map `crossProduct`, upgraded from linear to continuous-linear; useful for calculus. -/
 def crossProduct' : E →L[ℝ] E →L[ℝ] E :=
   LinearMap.toContinuousLinearMap
     (↑(LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] E) ≃ₗ[ℝ] E →L[ℝ] E) ∘ₗ ω.crossProduct)

diff --git a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.LinearAlgebra.Span
 
-/-! Note: some results should go to `linear_algebra.span`. -/
+/-! Note: some results should go to `LinearAlgebra.Span`. -/
 
 
 open Submodule Function