From 984e6f85d4110909b4284d535f41650ea1878205 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 8 Jun 2024 01:50:33 +0200
Subject: [PATCH] Update LinearMaps.lean

---
 HepLean/AnomalyCancellation/LinearMaps.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index f917b4c..3ed0bb8 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -9,7 +9,7 @@ import Mathlib.Algebra.BigOperators.Fin
 /-!
 # Linear maps
 
-Some definitions and properites of linear, bilinear, and trilinear maps, along with homogeneous
+Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous
 quadratic and cubic equations.
 
 ## TODO
@@ -62,7 +62,7 @@ instance instFun (V : Type) [AddCommMonoid V] [Module ℚ V] :
     cases g
     simp_all
 
-/-- The construction of a symmetric bilinear map from smul and map_add in the first factor,
+/-- The construction of a symmetric bilinear map from `smul` and `map_add` in the first factor,
 and swap. -/
 @[simps!]
 def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, T))
@@ -196,7 +196,7 @@ instance instFun : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ
     cases g
     simp_all
 
-/-- The construction of a symmetric trilinear map from smul and map_add in the first factor,
+/-- The construction of a symmetric trilinear map from `smul` and `map_add` in the first factor,
 and two swap. -/
 @[simps!]
 def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) = a * f (S, T, L))