[Merged by Bors] - chore: replace Lean 3 syntax λ x, in doc comments

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -638,8 +638,8 @@ theorem tendsto_integralSum_sum_integral (h : Integrable I l f vol) (π₀ : Pre
   exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU
 #align box_integral.integrable.tendsto_integral_sum_sum_integral BoxIntegral.Integrable.tendsto_integralSum_sum_integral
 
-/-- If `f` is integrable on `I`, then `λ J, integral J l f vol` is box-additive on subboxes of `I`:
-if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals
+/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of
+`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals
 of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`.
 
 See also `BoxIntegral.Integrable.toBoxAdditive` for a bundled version. -/
@@ -651,8 +651,8 @@ theorem sum_integral_congr (h : Integrable I l f vol) {π₁ π₂ : Prepartitio
   exact h.tendsto_integralSum_sum_integral π₂
 #align box_integral.integrable.sum_integral_congr BoxIntegral.Integrable.sum_integral_congr
 
-/-- If `f` is integrable on `I`, then `λ J, integral J l f vol` is box-additive on subboxes of `I`:
-if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals
+/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of
+`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals
 of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`.
 
 See also `BoxIntegral.Integrable.sum_integral_congr` for an unbundled version. -/

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -562,7 +562,7 @@ in any universe in `u, v, w, max u v, max v w, max u v w`, but it would be extre
 lead to a lot of duplication. Instead, we formulate the above proof when all spaces live in the same
 universe (where everything is fine), and then we deduce the general result by lifting all our spaces
 to a common universe. We use the trick that any space `H` is isomorphic through a continuous linear
-equiv to `ContinuousMultilinearMap (λ (i : Fin 0), E × F × G) H` to change the universe level,
+equiv to `ContinuousMultilinearMap (fun (i : Fin 0) ↦ E × F × G) H` to change the universe level,
 and then argue that composing with such a linear equiv does not change the fact of being `C^n`,
 which we have already proved previously.
 -/

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -639,7 +639,7 @@ variable {R : Type*} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpac
 open NormedRing ContinuousLinearMap Ring
 
 /-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the
-inversion operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/
+inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. -/
 theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) : HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x :=
   by simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx)
 #align has_fderiv_at_inv' hasFDerivAt_inv'

Mathlib/Analysis/Calculus/ParametricIntegral.lean

@@ -11,7 +11,7 @@ import Mathlib.MeasureTheory.Integral.SetIntegral
 /-!
 # Derivatives of integrals depending on parameters
 
-A parametric integral is a function with shape `f = λ x : H, ∫ a : α, F x a ∂μ` for some
+A parametric integral is a function with shape `f = fun x : H ↦ ∫ a : α, F x a ∂μ` for some
 `F : H → α → E`, where `H` and `E` are normed spaces and `α` is a measured space with measure `μ`.
 
 We already know from `continuous_of_dominated` in `Mathlib/MeasureTheory/Integral/Bochner.lean` how
@@ -31,8 +31,8 @@ variable.
   - `F x` is ae-measurable for x near `x₀`,
   - `F x₀` is integrable,
   - `fun x ↦ F x a` has derivative `F' a : H →L[ℝ] E` at `x₀` which is ae-measurable,
-  - `λ x, F x a` is locally Lipschitz near `x₀` for almost every `a`, with a Lipschitz bound which
-    is integrable with respect to `a`.
+  - `fun x ↦ F x a` is locally Lipschitz near `x₀` for almost every `a`,
+    with a Lipschitz bound which is integrable with respect to `a`.
 
   A subtle point is that the "near x₀" in the last condition has to be uniform in `a`. This is
   controlled by a positive number `ε`.

Mathlib/Analysis/Complex/OpenMapping.lean

@@ -21,8 +21,8 @@ its image `f z₀`. The results extend in higher dimension to `g : E → ℂ`.
 The proof of the local version on `ℂ` goes through two main steps: first, assuming that the function
 is not constant around `z₀`, use the isolated zero principle to show that `‖f z‖` is bounded below
 on a small `sphere z₀ r` around `z₀`, and then use the maximum principle applied to the auxiliary
-function `(λ z, ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`. That
-second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`.
+function `(fun z ↦ ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`.
+That second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`.
 
 ## Main results
 
@@ -45,7 +45,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball
     (hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖) (hz₀ : ∃ᶠ z in 𝓝 z₀, f z ≠ f z₀) :
     ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r := by
   /- This is a direct application of the maximum principle. Pick `v` close to `f z₀`, and look at
-    the function `λ z, ‖f z - v‖`: it is bounded below on the circle, and takes a small value
+    the function `fun z ↦ ‖f z - v‖`: it is bounded below on the circle, and takes a small value
     at `z₀` so it is not constant on the disk, which implies that its infimum is equal to `0` and
     hence that `v` is in the range of `f`. -/
   rintro v hv

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -129,7 +129,7 @@ section RpowDecay
 variable {E : Type*} [NormedAddCommGroup E]
 
 /-- If `f` is `O(x ^ (-b))` at infinity, then so is the function
-`λ x, ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`. -/
+`fun x ↦ ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`. -/
 theorem isBigO_norm_Icc_restrict_atTop {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
     (hf : f =O[atTop] fun x : ℝ => |x| ^ (-b)) (R S : ℝ) :
     (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atTop] fun x : ℝ => |x| ^ (-b) := by

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -35,11 +35,11 @@ equivalence to an inner-product space.
 ## Main results
 
 - `tendsto_integral_exp_inner_smul_cocompact` : for `V` a finite-dimensional real inner product
-  space and `f : V → E`, the function `λ w : V, ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f v` tends to 0
-  along `cocompact V`.
+  space and `f : V → E`, the function `fun w : V ↦ ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f v`
+  tends to 0 along `cocompact V`.
 - `tendsto_integral_exp_smul_cocompact` : for `V` a finite-dimensional real vector space (endowed
   with its unique Hausdorff topological vector space structure), and `W` the dual of `V`, the
-  function `λ w : W, ∫ v : V, exp (2 * π * w v * I) • f v` tends to along `cocompact W`.
+  function `fun w : W ↦ ∫ v : V, exp (2 * π * w v * I) • f v` tends to along `cocompact W`.
 - `Real.tendsto_integral_exp_smul_cocompact`: special case of functions on `ℝ`.
 - `Real.zero_at_infty_fourierIntegral` and `Real.zero_at_infty_vector_fourierIntegral`:
   reformulations explicitly using the Fourier integral.

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -2270,7 +2270,8 @@ end Continuous
 
 section ReApplyInnerSelf
 
-/-- Extract a real bilinear form from an operator `T`, by taking the pairing `λ x, re ⟪T x, x⟫`. -/
+/-- Extract a real bilinear form from an operator `T`,
+by taking the pairing `fun x ↦ re ⟪T x, x⟫`. -/
 def ContinuousLinearMap.reApplyInnerSelf (T : E →L[𝕜] E) (x : E) : ℝ :=
   re ⟪T x, x⟫
 #align continuous_linear_map.re_apply_inner_self ContinuousLinearMap.reApplyInnerSelf

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -95,8 +95,8 @@ def adjointDomain : Submodule 𝕜 F where
     exact hx.const_smul (conj a)
 #align linear_pmap.adjoint_domain LinearPMap.adjointDomain
 
-/-- The operator `λ x, ⟪y, T x⟫` considered as a continuous linear operator from `T.adjointDomain`
-to `𝕜`. -/
+/-- The operator `fun x ↦ ⟪y, T x⟫` considered as a continuous linear operator
+from `T.adjointDomain` to `𝕜`. -/
 def adjointDomainMkCLM (y : T.adjointDomain) : T.domain →L[𝕜] 𝕜 :=
   ⟨(innerₛₗ 𝕜 (y : F)).comp T.toFun, y.prop⟩
 #align linear_pmap.adjoint_domain_mk_clm LinearPMap.adjointDomainMkCLM

Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

@@ -15,18 +15,18 @@ import Mathlib.LinearAlgebra.Eigenspace.Basic
 # The Rayleigh quotient
 
 The Rayleigh quotient of a self-adjoint operator `T` on an inner product space `E` is the function
-`λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`.
+`fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2`.
 
 The main results of this file are `IsSelfAdjoint.hasEigenvector_of_isMaxOn` and
 `IsSelfAdjoint.hasEigenvector_of_isMinOn`, which state that if `E` is complete, and if the
 Rayleigh quotient attains its global maximum/minimum over some sphere at the point `x₀`, then `x₀`
-is an eigenvector of `T`, and the `iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2` is the corresponding
+is an eigenvector of `T`, and the `iSup`/`iInf` of `fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2` is the corresponding
 eigenvalue.
 
 The corollaries `LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` and
 `LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` state that if `E` is
 finite-dimensional and nontrivial, then `T` has some (nonzero) eigenvectors with eigenvalue the
-`iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`.
+`iSup`/`iInf` of `fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2`.
 
 ## TODO
 
@@ -125,7 +125,7 @@ theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F}
     ext x
     simp [dist_eq_norm]
   -- find Lagrange multipliers for the function `T.re_apply_inner_self` and the
-  -- hypersurface-defining function `λ x, ‖x‖ ^ 2`
+  -- hypersurface-defining function `fun x ↦ ‖x‖ ^ 2`
   obtain ⟨a, b, h₁, h₂⟩ :=
     IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀)
       (hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀)

Mathlib/Analysis/NormedSpace/Star/Exponential.lean

@@ -8,8 +8,8 @@ import Mathlib.Analysis.NormedSpace.Exponential
 #align_import analysis.normed_space.star.exponential from "leanprover-community/mathlib"@"1e3201306d4d9eb1fd54c60d7c4510ad5126f6f9"
 
 /-! # The exponential map from selfadjoint to unitary
-In this file, we establish various properties related to the map `λ a, exp ℂ A (I • a)` between the
-subtypes `selfAdjoint A` and `unitary A`.
+In this file, we establish various properties related to the map `fun a ↦ exp ℂ A (I • a)`
+between the subtypes `selfAdjoint A` and `unitary A`.
 
 ## TODO
 

Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

@@ -99,8 +99,8 @@ variable [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A]
 
 Because the multiplier algebra is defined as the algebra of double centralizers, there is a natural
 injection `DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ`
-defined by `λ a, (a.fst, MulOpposite.op a.snd)`. We use this map to pull back the ring, module and
-algebra structure from `(A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` to `𝓜(𝕜, A)`. -/
+defined by `fun a ↦ (a.fst, MulOpposite.op a.snd)`. We use this map to pull back the ring, module
+and algebra structure from `(A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` to `𝓜(𝕜, A)`. -/
 
 variable {𝕜 A}
 

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -58,7 +58,7 @@ theorem integral_exp_neg_Ioi_zero : (∫ x : ℝ in Ioi 0, exp (-x)) = 1 := by
   simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0
 #align integral_exp_neg_Ioi_zero integral_exp_neg_Ioi_zero
 
-/-- If `0 < c`, then `(λ t : ℝ, t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
+/-- If `0 < c`, then `(fun t : ℝ ↦ t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
 theorem integrableOn_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :
     IntegrableOn (fun t : ℝ => t ^ a) (Ioi c) := by
   have hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x := by

Mathlib/CategoryTheory/Adjunction/Reflective.lean

@@ -122,8 +122,8 @@ theorem unitCompPartialBijectiveAux_symm_apply [Reflective i] {A : C} {B : D}
 
 /-- If `i` has a reflector `L`, then the function `(i.obj (L.obj A) ⟶ B) → (A ⟶ B)` given by
 precomposing with `η.app A` is a bijection provided `B` is in the essential image of `i`.
-That is, the function `λ (f : i.obj (L.obj A) ⟶ B), η.app A ≫ f` is bijective, as long as `B` is in
-the essential image of `i`.
+That is, the function `fun (f : i.obj (L.obj A) ⟶ B) ↦ η.app A ≫ f` is bijective,
+as long as `B` is in the essential image of `i`.
 This definition gives an equivalence: the key property that the inverse can be described
 nicely is shown in `unitCompPartialBijective_symm_apply`.
 

Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

@@ -429,8 +429,8 @@ theorem Cotrident.IsColimit.homIso_natural [Nonempty J] {t : Cotrident f} {Z Z'
 
 /-- This is a helper construction that can be useful when verifying that a category has certain wide
     equalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
-    `parallelFamily (λ j, F.map (line j))`, and a trident on `λ j, F.map (line j)`, we get a cone
-    on `F`.
+    `parallelFamily (λ j, F.map (line j))`, and a trident on `fun j ↦ F.map (line j)`,
+    we get a cone on `F`.
 
     If you're thinking about using this, have a look at
     `hasWideEqualizers_of_hasLimit_parallelFamily`, which you may find to be an easier way of

Mathlib/Data/Matrix/Basic.lean

@@ -41,8 +41,8 @@ The locale `Matrix` gives the following notation:
 
 For convenience, `Matrix m n α` is defined as `m → n → α`, as this allows elements of the matrix
 to be accessed with `A i j`. However, it is not advisable to _construct_ matrices using terms of the
-form `λ i j, _` or even `(λ i j, _ : Matrix m n α)`, as these are not recognized by lean as having
-the right type. Instead, `Matrix.of` should be used.
+form `fun i j ↦ _` or even `(fun i j ↦ _ : Matrix m n α)`, as these are not recognized by Lean
+as having the right type. Instead, `Matrix.of` should be used.
 
 ## TODO
 

Mathlib/Data/Ordmap/Ordnode.lean

@@ -596,7 +596,7 @@ Case conversion may be inaccurate. Consider using '#align ordnode.map Ordnode.ma
 the function is strictly monotone, i.e. `x < y → f x < f y`.
 
      partition (fun x ↦ x + 2) {1, 2, 4} = {2, 3, 6}
-     partition (λ x : ℕ, x - 2) {1, 2, 4} = precondition violation -/
+     partition (fun x : ℕ ↦ x - 2) {1, 2, 4} = precondition violation -/
 def map {β} (f : α → β) : Ordnode α → Ordnode β
   | nil => nil
   | node s l x r => node s (map f l) (f x) (map f r)

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -161,7 +161,7 @@ theorem toEquiv_inj {h h' : M ≃ₘ^n⟮I, I'⟯ M'} : h.toEquiv = h'.toEquiv 
   toEquiv_injective.eq_iff
 #align diffeomorph.to_equiv_inj Diffeomorph.toEquiv_inj
 
-/-- Coercion to function `λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M')` is injective. -/
+/-- Coercion to function `fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M')` is injective. -/
 theorem coeFn_injective : Injective ((↑) : (M ≃ₘ^n⟮I, I'⟯ M') → (M → M')) :=
   DFunLike.coe_injective
 #align diffeomorph.coe_fn_injective Diffeomorph.coeFn_injective

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -89,7 +89,7 @@ variable (ι M)
 /-- We say that a collection of `SmoothBumpFunction`s is a `SmoothBumpCovering` of a set `s` if
 
 * `(f i).c ∈ s` for all `i`;
-* the family `λ i, support (f i)` is locally finite;
+* the family `fun i ↦ support (f i)` is locally finite;
 * for each point `x ∈ s` there exists `i` such that `f i =ᶠ[𝓝 x] 1`;
   in other words, `x` belongs to the interior of `{y | f i y = 1}`;
 
@@ -116,7 +116,7 @@ structure SmoothBumpCovering (s : Set M := univ) where
 /-- We say that a collection of functions form a smooth partition of unity on a set `s` if
 
 * all functions are infinitely smooth and nonnegative;
-* the family `λ i, support (f i)` is locally finite;
+* the family `fun i ↦ support (f i)` is locally finite;
 * for all `x ∈ s` the sum `∑ᶠ i, f i x` equals one;
 * for all `x`, the sum `∑ᶠ i, f i x` is less than or equal to one. -/
 structure SmoothPartitionOfUnity (s : Set M := univ) where
@@ -196,7 +196,7 @@ theorem smooth_smul {g : M → F} {i} (hg : ∀ x ∈ tsupport (f i), SmoothAt I
 
 /-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of
 functions such that `g i` is $C^n$ smooth at every point of the topological support of `f i`, then
-the sum `λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
+the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
 theorem contMDiff_finsum_smul {g : ι → M → F}
     (hg : ∀ (i), ∀ x ∈ tsupport (f i), ContMDiffAt I 𝓘(ℝ, F) n (g i) x) :
     ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x :=
@@ -206,7 +206,7 @@ theorem contMDiff_finsum_smul {g : ι → M → F}
 
 /-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of
 functions such that `g i` is smooth at every point of the topological support of `f i`, then the sum
-`λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
+`fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
 theorem smooth_finsum_smul {g : ι → M → F}
     (hg : ∀ (i), ∀ x ∈ tsupport (f i), SmoothAt I 𝓘(ℝ, F) (g i) x) :
     Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ i, f i x • g i x :=
@@ -310,7 +310,7 @@ alias ⟨_, IsSubordinate.toPartitionOfUnity⟩ := isSubordinate_toPartitionOfUn
 
 /-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets
 `U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is $C^n$ smooth on
-`U i`, then the sum `λ x, ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold. -/
+`U i`, then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold. -/
 theorem IsSubordinate.contMDiff_finsum_smul {g : ι → M → F} (hf : f.IsSubordinate U)
     (ho : ∀ i, IsOpen (U i)) (hg : ∀ i, ContMDiffOn I 𝓘(ℝ, F) n (g i) (U i)) :
     ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x :=
@@ -319,7 +319,7 @@ theorem IsSubordinate.contMDiff_finsum_smul {g : ι → M → F} (hf : f.IsSubor
 
 /-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets
 `U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is smooth on `U i`,
-then the sum `λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
+then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
 theorem IsSubordinate.smooth_finsum_smul {g : ι → M → F} (hf : f.IsSubordinate U)
     (ho : ∀ i, IsOpen (U i)) (hg : ∀ i, SmoothOn I 𝓘(ℝ, F) (g i) (U i)) :
     Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ i, f i x • g i x :=

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

@@ -128,10 +128,10 @@ def toLinear : GeneralLinearGroup n R ≃* LinearMap.GeneralLinearGroup R (n →
   Units.mapEquiv Matrix.toLinAlgEquiv'.toRingEquiv.toMulEquiv
 #align matrix.general_linear_group.to_linear Matrix.GeneralLinearGroup.toLinear
 
--- Note that without the `@` and `‹_›`, lean infers `λ a b, _inst a b` instead of `_inst` as the
+-- Note that without the `@` and `‹_›`, Lean infers `fun a b ↦ _inst a b` instead of `_inst` as the
 -- decidability argument, which prevents `simp` from obtaining the instance by unification.
--- These `λ a b, _inst a b` terms also appear in the type of `A`, but simp doesn't get confused by
--- them so for now we do not care.
+-- These `fun a b ↦ _inst a b` terms also appear in the type of `A`, but simp doesn't get confused
+-- by them so for now we do not care.
 @[simp]
 theorem coe_toLinear : (@toLinear n ‹_› ‹_› _ _ A : (n → R) →ₗ[R] n → R) = Matrix.mulVecLin A :=
   rfl