DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update LinearMaps.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 01:50:33 +02:00
parent 2425c09e87
commit 984e6f85d4
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/LinearMaps.lean
View file

@ -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))