chore: fix spelling mistakes

Author: euprunin

FLT/ForMathlib/ActionTopology.lean

@@ -155,7 +155,7 @@ instance instId (R : Type*) [Semiring R] [τR : TopologicalSpace R] [Topological
   /- Let `R` be a topological ring with topology τR. To prove that `τR` is the action
   topology, it suffices to prove inclusions in both directions.
   One way is obvious: addition and multiplication are continuous for `R`, so the
-  action topology is finer than `R` because it's the finest topology wih these properties.-/
+  action topology is finer than `R` because it's the finest topology with these properties.-/
   refine le_antisymm ?_ (actionTopology_le R R)
   /- The other way is more interesting. We can interpret the problem as proving that
   the identity function is continuous from `R` with the action topology to `R` with

FLT/HIMExperiments/ContinuousSMul_topology.lean

@@ -35,9 +35,9 @@ In the module case one could demand that all `R`-linear maps `A →ₗ[R] R`
 are continuous. But the definition here is one proposed by Yury
 Kudryashov. He pointed out that if `τᵢ : TopologicalSpace A` all make
 the action maps `R × A → A` continuous, then the `Inf` of the `τᵢ`
-also has this proprty. This means that there is a smallest (in the `≤` sense,
+also has this property. This means that there is a smallest (in the `≤` sense,
 i.e. the most open sets) topology on `A` such that `• : R × A → A` is
-continous. We call topology the *action topology*. It is some kind
+continuous. We call topology the *action topology*. It is some kind
 of "pushforward topology" on `A` coming from the `R`-action, but
 it is not a pushforward in the `f_*` sense of the word because
 there is no fixed `f : R → A`.
@@ -182,7 +182,7 @@ variable {R : Type} [τR : TopologicalSpace R]
 -- let `M` and `N` have an action of `R`
 -- We do not need Mul on R, but there seems to be no class saying just 1 • m = m
 -- so we have to use MulAction
---variable [Monoid R] -- no ContinuousMul becasuse we never need
+--variable [Monoid R] -- no ContinuousMul because we never need
 -- we do not need MulAction because we do not need mul_smul.
 -- We only need one_smul
 variable {M : Type} [Zero M] [SMul R M] [aM : TopologicalSpace M] [IsActionTopology R M]
@@ -192,7 +192,7 @@ open TopologicalSpace in
 lemma prod [MulOneClass.{0} R] : IsActionTopology.{0} R (M × N) := by
   constructor
   -- goal: to prove product topology is action topology.
-  -- Well product topology will obviously have continuous_smul becasue
+  -- Well product topology will obviously have continuous_smul because
   -- of continuous_smulprod or whatever, assuming that exists.
   --unfold instTopologicalSpaceProd actionTopology
   apply le_antisymm

FLT/HIMExperiments/dual_topology.lean

@@ -43,9 +43,9 @@ In the module case one could demand that all `R`-linear maps `A →ₗ[R] R`
 are continuous. But the definition here is one proposed by Yury
 Kudryashov. He pointed out that if `τᵢ : TopologicalSpace A` all make
 the action maps `R × A → A` continuous, then the `Inf` of the `τᵢ`
-also has this proprty. This means that there is a smallest (in the `≤` sense,
+also has this property. This means that there is a smallest (in the `≤` sense,
 i.e. the most open sets) topology on `A` such that `• : R × A → A` is
-continous. We call topology the *action topology*. It is some kind
+continuous. We call topology the *action topology*. It is some kind
 of "pushforward topology" on `A` coming from the `R`-action, but
 it is not a pushforward in the `f_*` sense of the word because
 there is no fixed `f : R → A`.

FLT/HIMExperiments/module_topology.lean

@@ -75,7 +75,7 @@ variable {N : Type*} [AddCommGroup N] [Module A N]
 /-- The "canonical topology" on a module `M` over a topological ring `A`. It's defined as
 the weakest topology on `M` which makes every `A`-linear map `M → A` continuous. -/
 -- make it an abbreviation not a definition; this means that Lean "prints `Module.topology`
--- in the tactic state for the human reader" but interally is syntactically equal to
+-- in the tactic state for the human reader" but internally is syntactically equal to
 -- to the `iInf`, meaning that all the `iInf` rewrites still work.
 abbrev Module.topology : TopologicalSpace M :=
 -- Topology defined as greatest lower bound of pullback topologies. So it's the biggest

FLT/HIMExperiments/right_module_topology.lean

@@ -57,7 +57,7 @@ section one
 
 variable {R : Type*} [τR : TopologicalSpace R]
 
--- this proof shoudl be much easier
+-- this proof should be much easier
 example [Monoid R] [ContinuousMul R] :
     IsActionTopology R R where
   isActionTopology' := by
@@ -79,7 +79,7 @@ example [Monoid R] [ContinuousMul R] :
       convert hσ
       simp only [smul_eq_mul, mul_one]
       rfl
--- this proof shoudl be much easier
+-- this proof should be much easier
 end one
 
 section type_stuff

blueprint/src/util.sty

@@ -103,7 +103,7 @@
 \definecolor{param_col}{RGB}{206, 120, 232}
 \definecolor{ih_col}{RGB}{232, 191, 120}
 
-% we don't have `frame hidden` since we can't use `skins` from tcolorbox withou compile errors
+% we don't have `frame hidden` since we can't use `skins` from tcolorbox without compile errors
 \tcolorboxenvironment{definition}{colback=def_col!30,colframe=white,breakable,arc=0mm}
 \tcolorboxenvironment{claim}{colback=lemma_col!30,colframe=white,breakable,arc=0mm}
 \tcolorboxenvironment{proposition}{colback=lemma_col!30,colframe=white,breakable,arc=0mm}