chore: fix upper/lowercase in comments (#4360)

* Run a non-interactive version of `fix-comments.py` on all files.
* Go through the diff and manually add/discard/edit chunks.

Mathlib/Algebra/BigOperators/Basic.lean

@@ -280,7 +280,7 @@ theorem MonoidHom.coe_finset_prod [MulOneClass β] [CommMonoid γ] (f : α → 
 #align monoid_hom.coe_finset_prod MonoidHom.coe_finset_prod
 #align add_monoid_hom.coe_finset_sum AddMonoidHom.coe_finset_sum
 
--- See also `finset.prod_apply`, with the same conclusion
+-- See also `Finset.prod_apply`, with the same conclusion
 -- but with the weaker hypothesis `f : α → β → γ`.
 @[to_additive (attr := simp)]
 theorem MonoidHom.finset_prod_apply [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α)
@@ -761,8 +761,8 @@ theorem prod_filter_of_ne {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s,
 #align finset.prod_filter_of_ne Finset.prod_filter_of_ne
 #align finset.sum_filter_of_ne Finset.sum_filter_of_ne
 
--- If we use `[decidable_eq β]` here, some rewrites fail because they find a wrong `decidable`
--- instance first; `{∀ x, decidable (f x ≠ 1)}` doesn't work with `rw ← prod_filter_ne_one`
+-- If we use `[DecidableEq β]` here, some rewrites fail because they find a wrong `Decidable`
+-- instance first; `{∀ x, Decidable (f x ≠ 1)}` doesn't work with `rw ← prod_filter_ne_one`
 @[to_additive]
 theorem prod_filter_ne_one [∀ x, Decidable (f x ≠ 1)] :
     (∏ x in s.filter fun x => f x ≠ 1, f x) = ∏ x in s, f x :=
@@ -1089,7 +1089,7 @@ theorem prod_ite_eq [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
 /-- A product taken over a conditional whose condition is an equality test on the index and whose
 alternative is `1` has value either the term at that index or `1`.
 
-The difference with `Finset.prod_ite_eq` is that the arguments to `eq` are swapped. -/
+The difference with `Finset.prod_ite_eq` is that the arguments to `Eq` are swapped. -/
 @[to_additive (attr := simp) "A sum taken over a conditional whose condition is an equality
 test on the index and whose alternative is `0` has value either the term at that index or `0`.
 
@@ -2279,7 +2279,7 @@ theorem nat_abs_sum_le {ι : Type _} (s : Finset ι) (f : ι → ℤ) :
       exact (Int.natAbs_add_le _ _).trans (add_le_add le_rfl IH)
 #align nat_abs_sum_le nat_abs_sum_le
 
-/-! ### `additive`, `multiplicative` -/
+/-! ### `Additive`, `Multiplicative` -/
 
 
 open Additive Multiplicative

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -940,7 +940,7 @@ theorem finprod_mem_image {s : Set β} {g : β → α} (hg : s.InjOn g) :
 #align finprod_mem_image finprod_mem_image
 #align finsum_mem_image finsum_mem_image
 
-/-- The product of `f y` over `y ∈ set.range g` equals the product of `f (g i)` over all `i`
+/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
 provided that `g` is injective on `mulSupport (f ∘ g)`. -/
 @[to_additive
       "The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`

Mathlib/Algebra/BigOperators/Order.lean

@@ -569,7 +569,7 @@ theorem prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g
 #align finset.prod_le_prod Finset.prod_le_prod
 
 /-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
-See also `finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
+See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
 theorem prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : (∏ i in s, f i) ≤ 1 := by
   convert ← prod_le_prod h0 h1
   exact Finset.prod_const_one

Mathlib/Algebra/CharP/Algebra.lean

@@ -65,7 +65,7 @@ As an application, a `ℚ`-algebra has characteristic zero.
 
 
 -- `CharP.charP_to_charZero A _ (charP_of_injective_algebraMap h 0)` does not work
--- here as it would require `ring A`.
+-- here as it would require `Ring A`.
 section QAlgebra
 
 variable (R : Type _) [Nontrivial R]

Mathlib/Algebra/CharP/LocalRing.lean

@@ -60,7 +60,7 @@ theorem charP_zero_or_prime_power (R : Type _) [CommRing R] [LocalRing R] (q : 
     have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q
     have n_pos : n ≠ 0 := fun n_zero =>
       absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
-    -- Definition of prime power: `∃ r n, prime r ∧ 0 < n ∧ r ^ n = q`.
+    -- Definition of prime power: `∃ r n, Prime r ∧ 0 < n ∧ r ^ n = q`.
     exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
   · haveI K_char_p_0 := ringChar.of_eq r_zero
     haveI K_char_zero : CharZero K := CharP.charP_to_charZero K

Mathlib/Algebra/CharP/Two.lean

@@ -16,7 +16,7 @@ import Mathlib.Algebra.CharP.Basic
 This file contains results about `CharP R 2`, in the `CharTwo` namespace.
 
 The lemmas in this file with a `_sq` suffix are just special cases of the `_pow_char` lemmas
-elsewhere, with a shorter name for ease of discovery, and no need for a `[Fact (prime 2)]` argument.
+elsewhere, with a shorter name for ease of discovery, and no need for a `[Fact (Prime 2)]` argument.
 -/
 
 

Mathlib/Algebra/CovariantAndContravariant.lean

@@ -60,7 +60,7 @@ as it is easier to use.
 -/
 
 
--- TODO: convert `has_exists_mul_of_le`, `has_exists_add_of_le`?
+-- TODO: convert `ExistsMulOfLE`, `ExistsAddOfLE`?
 -- TODO: relationship with `Con/AddCon`
 -- TODO: include equivalence of `LeftCancelSemigroup` with
 -- `Semigroup PartialOrder ContravariantClass α α (*) (≤)`?
@@ -263,7 +263,7 @@ theorem Monotone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Mo
 #align monotone.covariant_of_const Monotone.covariant_of_const
 
 /-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
-the operator.  E.g., `∀ (m : ℕ), monotone f → monotone (λ n, f (n + m))`. -/
+the operator.  E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (n + m))`. -/
 theorem Monotone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
     (hf : Monotone f) (m : N) : Monotone fun n ↦ f (μ n m) :=
   fun _ _ x ↦ hf (@Covariant.monotone_of_const _ _ (swap μ) _ _ m _ _ x)

Mathlib/Algebra/DirectSum/Ring.lean

@@ -70,7 +70,7 @@ instances for:
 
 If `CompleteLattice.independent (Set.range A)`, these provide a gradation of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
-`DirectSum.toMonoid (λ i, AddSubmonoid.inclusion $ le_supr A i)`.
+`DirectSum.toMonoid (λ i, AddSubmonoid.inclusion $ le_iSup A i)`.
 
 ## tags
 
@@ -171,7 +171,7 @@ variable [Add ι] [∀ i, AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A]
 
 open AddMonoidHom (flip_apply coe_comp compHom)
 
-/-- The piecewise multiplication from the `has_mul` instance, as a bundled homomorphism. -/
+/-- The piecewise multiplication from the `Mul` instance, as a bundled homomorphism. -/
 @[simps]
 def gMulHom {i j} : A i →+ A j →+ A (i + j) where
   toFun a :=

Mathlib/Algebra/DualNumber.lean

@@ -102,7 +102,7 @@ variable {A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
 /-- A universal property of the dual numbers, providing a unique `R[ε] →ₐ[R] A` for every element
 of `A` which squares to `0`.
 
-This isomorphism is named to match the very similar `complex.lift`. -/
+This isomorphism is named to match the very similar `Complex.lift`. -/
 @[simps!]
 def lift : { e : A // e * e = 0 } ≃ (R[ε] →ₐ[R] A) :=
   Equiv.trans

Mathlib/Algebra/Free.lean

@@ -24,7 +24,7 @@ import Mathlib.Data.List.Basic
   defined inductively, with traversable instance and decidable equality.
 * `MagmaAssocQuotient α`: quotient of a magma `α` by the associativity equivalence relation.
 * `FreeSemigroup α`: free semigroup over alphabet `α`, defined as a structure with two fields
-  `head : α` and `tail : list α` (i.e. nonempty lists), with traversable instance and decidable
+  `head : α` and `tail : List α` (i.e. nonempty lists), with traversable instance and decidable
   equality.
 * `FreeMagmaAssocQuotientEquiv α`: isomorphism between `MagmaAssocQuotient (FreeMagma α)` and
   `FreeSemigroup α`.

Mathlib/Algebra/GradedMonoid.lean

@@ -175,7 +175,7 @@ macro "apply_gmonoid_gnpowRec_zero_tac" : tactic => `(tactic | apply GMonoid.gnp
 /-- A tactic to for use as an optional value for `Gmonoid.gnpow_succ'' -/
 macro "apply_gmonoid_gnpowRec_succ_tac" : tactic => `(tactic | apply GMonoid.gnpowRec_succ)
 
-/-- A graded version of `monoid`
+/-- A graded version of `Monoid`
 
 Like `Monoid.npow`, this has an optional `GMonoid.gnpow` field to allow definitional control of
 natural powers of a graded monoid. -/
@@ -383,7 +383,7 @@ theorem List.dProdIndex_eq_map_sum (l : List α) (fι : α → ι) :
 /-- A dependent product for graded monoids represented by the indexed family of types `A i`.
 This is a dependent version of `(l.map fA).prod`.
 
-For a list `l : list α`, this computes the product of `fA a` over `a`, where each `fA` is of type
+For a list `l : List α`, this computes the product of `fA a` over `a`, where each `fA` is of type
 `A (fι a)`. -/
 def List.dProd (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) : A (l.dProdIndex fι) :=
   l.foldrRecOn _ _ GradedMonoid.GOne.one fun _ x a _ => GradedMonoid.GMul.mul (fA a) x

Mathlib/Algebra/Group/Conj.lean

@@ -144,7 +144,7 @@ theorem isConj_iff₀ [GroupWithZero α] {a b : α} : IsConj a b ↔ ∃ c : α,
 
 namespace IsConj
 
-/- This small quotient API is largely copied from the API of `associates`;
+/- This small quotient API is largely copied from the API of `Associates`;
 where possible, try to keep them in sync -/
 /-- The setoid of the relation `IsConj` iff there is a unit `u` such that `u * x = y * u` -/
 protected def setoid (α : Type _) [Monoid α] : Setoid α where
@@ -235,7 +235,7 @@ Since `Multiset` and `Con.quotient` are both quotient types, unification will ch
 that the relations `List.perm` and `c.toSetoid.r` unify. However, `c.toSetoid` depends on
 a `Mul M` instance, so this unification triggers a search for `Mul (List α)`;
 this will traverse all subclasses of `Mul` before failing.
-On the other hand, the search for an instance of `DecidableEq (Con.quotient c)` for `c : con M`
+On the other hand, the search for an instance of `DecidableEq (Con.quotient c)` for `c : Con M`
 can quickly reject the candidate instance `Multiset.decidableEq` because the type of
 `List.perm : List ?m_1 → List ?m_1 → Prop` does not unify with `M → M → Prop`.
 Therefore, we should assign `Con.quotient.decidableEq` a lower priority because it fails slowly.

Mathlib/Algebra/Group/Defs.lean

@@ -791,7 +791,7 @@ Those two pairs of made-up classes fulfill slightly different roles.
 `ℤ` action (`zpow` or `zsmul`). Further, it provides a `div` field, matching the forgetful
 inheritance pattern. This is useful to shorten extension clauses of stronger structures (`Group`,
 `GroupWithZero`, `DivisionRing`, `Field`) and for a few structures with a rather weak
-pseudo-inverse (`matrix`).
+pseudo-inverse (`Matrix`).
 
 `DivisionMonoid`/`SubtractionMonoid` is targeted at structures with stronger pseudo-inverses. It
 is an ad hoc collection of axioms that are mainly respected by three things:
@@ -804,7 +804,7 @@ multiplication, except for the fact that it might not be a true inverse (`a / a
 The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are
 independent:
 * Without `DivisionMonoid.div_eq_mul_inv`, you can define `/` arbitrarily.
-* Without `DivisionMonoid.inv_inv`, you can consider `WithTop unit` with `a⁻¹ = ⊤` for all `a`.
+* Without `DivisionMonoid.inv_inv`, you can consider `WithTop Unit` with `a⁻¹ = ⊤` for all `a`.
 * Without `DivisionMonoid.mul_inv_rev`, you can consider `WithTop α` with `a⁻¹ = a` for all `a`
   where `α` non commutative.
 * Without `DivisionMonoid.inv_eq_of_mul`, you can consider any `CommMonoid` with `a⁻¹ = a` for all

Mathlib/Algebra/Group/OrderSynonym.lean

@@ -14,7 +14,7 @@ import Mathlib.Order.Synonym
 /-!
 # Group structure on the order type synonyms
 
-Transfer algebraic instances from `α` to `αᵒᵈ` and `lex α`.
+Transfer algebraic instances from `α` to `αᵒᵈ` and `Lex α`.
 -/
 
 

Mathlib/Algebra/Group/Prod.lean

@@ -18,7 +18,7 @@ import Mathlib.Algebra.Hom.Units
 In this file we define one-binop (`Monoid`, `Group` etc) structures on `M × N`. We also prove
 trivial `simp` lemmas, and define the following operations on `MonoidHom`s:
 
-* `fst M N : M × N →* M`, `snd M N : M × N →* N`: projections `prod.fst` and `prod.snd`
+* `fst M N : M × N →* M`, `snd M N : M × N →* N`: projections `Prod.fst` and `Prod.snd`
   as `MonoidHom`s;
 * `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid
   into the product;

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -25,8 +25,8 @@ information about these structures (which are not that standard in informal math
 ## Porting notes
 
 In Lean 3, we use `id` here and there to get correct types of proofs. This is required because
-`with_one` and `with_zero` are marked as `irreducible` at the end of `algebra.group.with_one.defs`,
-so proofs that use `option α` instead of `with_one α` no longer typecheck. In Lean 4, both types are
+`WithOne` and `WithZero` are marked as `Irreducible` at the end of `algebra.group.with_one.defs`,
+so proofs that use `Option α` instead of `WithOne α` no longer typecheck. In Lean 4, both types are
 plain `def`s, so we don't need these `id`s.
 -/
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -221,7 +221,7 @@ instance NeZero.one : NeZero (1 : M₀) := ⟨by
 
 variable {M₀}
 
-/-- Pullback a `nontrivial` instance along a function sending `0` to `0` and `1` to `1`. -/
+/-- Pullback a `Nontrivial` instance along a function sending `0` to `0` and `1` to `1`. -/
 theorem pullback_nonzero [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) :
     Nontrivial M₀' :=
   ⟨⟨0, 1, mt (congr_arg f) <| by

Mathlib/Algebra/Hom/NonUnitalAlg.lean

@@ -409,7 +409,7 @@ end Prod
 
 end NonUnitalAlgHom
 
-/-! ### Interaction with `alg_hom` -/
+/-! ### Interaction with `AlgHom` -/
 
 
 namespace AlgHom

Mathlib/Algebra/Homology/Homotopy.lean

@@ -444,7 +444,7 @@ theorem nullHomotopicMap'_f_eq_zero {k₀ : ι} (hk₀ : ∀ l : ι, ¬c.Rel k
 so that as we construct each component, we have available the previous two components,
 and the fact that they satisfy the homotopy condition.
 
-To simplify the situation, we only construct homotopies of the form `homotopy e 0`.
+To simplify the situation, we only construct homotopies of the form `Homotopy e 0`.
 `Homotopy.equivSubZero` can provide the general case.
 
 Notice however, that this construction does not have particularly good definitional properties:

Mathlib/Algebra/Invertible.lean

@@ -44,7 +44,7 @@ users can choose which instances to use at the point of use.
 
 For example, here's how you can use an `Invertible 1` instance:
 ```lean
-variables {α : Type _} [monoid α]
+variables {α : Type _} [Monoid α]
 
 def something_that_needs_inverses (x : α) [Invertible x] := sorry
 
@@ -180,7 +180,7 @@ def Invertible.copy [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs :
 theorem Invertible.congr [Ring α] (a b : α) [Invertible a] [Invertible b] (h : a = b) :
   ⅟a = ⅟b := by subst h; congr; apply Subsingleton.allEq
 
-/-- An `invertible` element is a unit. -/
+/-- An `Invertible` element is a unit. -/
 @[simps]
 def unitOfInvertible [Monoid α] (a : α) [Invertible a] :
     αˣ where
@@ -435,7 +435,7 @@ def Invertible.map {R : Type _} {S : Type _} {F : Type _} [MulOneClass R] [MulOn
   mul_invOf_self := by rw [← map_mul, mul_invOf_self, map_one]
 #align invertible.map Invertible.map
 
-/-- Note that the `invertible (f r)` argument can be satisfied by using `letI := invertible.map f r`
+/-- Note that the `Invertible (f r)` argument can be satisfied by using `letI := Invertible.map f r`
 before applying this lemma. -/
 theorem map_invOf {R : Type _} {S : Type _} {F : Type _} [MulOneClass R] [Monoid S]
     [MonoidHomClass F R S] (f : F) (r : R) [Invertible r] [ifr : Invertible (f r)] :

Mathlib/Algebra/Lie/Basic.lean

@@ -82,7 +82,7 @@ class LieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] extends Modu
 
 /-- A Lie ring module is an additive group, together with an additive action of a
 Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
-(For representations of Lie *algebras* see `lie_module`.) -/
+(For representations of Lie *algebras* see `LieModule`.) -/
 /- @[protect_proj] -- Porting note: not (yet) implemented. -/
 class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] extends Bracket L M where
   /-- A Lie ring module bracket is additive in its first component. -/

Mathlib/Algebra/Module/Basic.lean

@@ -28,7 +28,7 @@ In this file we define
 ## Implementation notes
 
 In typical mathematical usage, our definition of `Module` corresponds to "semimodule", and the
-word "module" is reserved for `Module R M` where `R` is a `ring` and `M` an `AddCommGroup`.
+word "module" is reserved for `Module R M` where `R` is a `Ring` and `M` an `AddCommGroup`.
 If `R` is a `Field` and `M` an `AddCommGroup`, `M` would be called an `R`-vector space.
 Since those assumptions can be made by changing the typeclasses applied to `R` and `M`,
 without changing the axioms in `Module`, mathlib calls everything a `Module`.

Mathlib/Algebra/Module/Equiv.lean

@@ -332,8 +332,8 @@ variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ
 -- we have to list all the variables explicitly here in order to match the Lean 3 signature.
 set_option linter.unusedVariables false in
 /-- Linear equivalences are transitive. -/
--- Note: the `ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
--- implicitly for lemmas like `linear_equiv.self_trans_symm`.
+-- Note: the `RingHomCompTriple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
+-- implicitly for lemmas like `LinearEquiv.self_trans_symm`.
 @[trans, nolint unusedArguments]
 def trans
     [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]

Mathlib/Algebra/Module/Injective.lean

@@ -30,7 +30,7 @@ import Mathlib.Data.TypeMax -- Porting note: added for universe issues
   Q
   ```
 * `Module.Baer`: an `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an
-  `ideal R` extends to an `R`-linear map `R ⟶  Q`
+  `Ideal R` extends to an `R`-linear map `R ⟶  Q`
 
 ## Main statements
 
@@ -89,7 +89,7 @@ theorem Module.injective_iff_injective_object :
     @Module.injective_module_of_injective_object R _ Q _ _ h⟩
 #align module.injective_iff_injective_object Module.injective_iff_injective_object
 
-/-- An `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an `ideal R` extends to
+/-- An `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an `Ideal R` extends to
 an `R`-linear map `R ⟶ Q`-/
 def Module.Baer : Prop :=
   ∀ (I : Ideal R) (g : I →ₗ[R] Q), ∃ g' : R →ₗ[R] Q, ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Mathlib/Algebra/Module/LinearMap.lean

@@ -98,7 +98,7 @@ structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R
   map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x
 #align linear_map LinearMap
 
-/-- The `add_hom` underlying a `LinearMap`. -/
+/-- The `AddHom` underlying a `LinearMap`. -/
 add_decl_doc LinearMap.toAddHom
 #align linear_map.to_add_hom LinearMap.toAddHom
 
@@ -141,7 +141,7 @@ attribute [simp] map_smulₛₗ
 
 /-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`.
 
-This is an abbreviation for `semilinear_map_class F (RingHom.id R) M M₂`.
+This is an abbreviation for `SemilinearMapClass F (RingHom.id R) M M₂`.
 -/
 abbrev LinearMapClass (F : Type _) (R M M₂ : outParam (Type _)) [Semiring R] [AddCommMonoid M]
     [AddCommMonoid M₂] [Module R M] [Module R M₂] :=
@@ -397,7 +397,7 @@ end Pointwise
 
 variable (M M₂)
 
-/-- A typeclass for `has_smul` structures which can be moved through a `LinearMap`.
+/-- A typeclass for `SMul` structures which can be moved through a `LinearMap`.
 This typeclass is generated automatically from a `IsScalarTower` instance, but exists so that
 we can also add an instance for `AddCommGroup.intModule`, allowing `z •` to be moved even if
 `R` does not support negation.
@@ -625,7 +625,7 @@ end LinearMap
 
 namespace Module
 
-/-- `g : R →+* S` is `R`-linear when the module structure on `S` is `module.comp_hom S g` . -/
+/-- `g : R →+* S` is `R`-linear when the module structure on `S` is `Module.compHom S g` . -/
 @[simps]
 def compHom.toLinearMap {R S : Type _} [Semiring R] [Semiring S] (g : R →+* S) :
     letI := compHom S g; R →ₗ[R] S :=
@@ -1115,7 +1115,7 @@ end
 /-! ### Action by a module endomorphism. -/
 
 
-/-- The tautological action by `module.End R M` (aka `M →ₗ[R] M`) on `M`.
+/-- The tautological action by `Module.End R M` (aka `M →ₗ[R] M`) on `M`.
 
 This generalizes `Function.End.applyMulAction`. -/
 instance applyModule : Module (Module.End R M) M