tidy-up

Author: harahu

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -754,7 +754,7 @@ theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃φ₁ φ₂ :
     (hs : s.EqOn φ₁ φ₂) : φ₁ = φ₂ :=
   ext fun _x => adjoin_le_equalizer φ₁ φ₂ hs <| h.symm ▸ trivial
 
-/-- Two algebra morphisms are equal on `Algebra.span s` iff they are equal on s -/
+/-- Two algebra morphisms are equal on `Algebra.span s` iff they are equal on `s`. -/
 theorem eqOn_adjoin_iff {φ ψ : A →ₐ[R] B} {s : Set A} :
     Set.EqOn φ ψ (adjoin R s) ↔ Set.EqOn φ ψ s := by
   have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl

Mathlib/GroupTheory/GroupAction/Hom.lean

@@ -801,7 +801,7 @@ class MulSemiringActionSemiHomClass (F : Type*)
     extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S
 
 /-- `MulSemiringActionHomClass F M R S` states that `F` is a type of morphisms preserving
-the ring structure and equivariant with respect to a `DistribMulAction` of `M` on `R` and `S` .
+the ring structure and equivariant with respect to a `DistribMulAction` of `M` on `R` and `S`.
 -/
 abbrev MulSemiringActionHomClass
     (F : Type*)

Mathlib/RingTheory/Conductor.lean

@@ -12,7 +12,7 @@ public import Mathlib.RingTheory.PowerBasis
 # The conductor ideal
 This file defines the conductor ideal of an element `x` of `R`-algebra `S`. This is the ideal of
 `S` consisting of all elements `a` such that for all `b` in `S`, the product `a * b` lies in the
-`R` subalgebra of `S` generated by `x`.
+`R`-subalgebra of `S` generated by `x`.
 
 -/