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

Docs

Browse source
This commit is contained in:
jstoobysmith 2024-04-17 06:38:25 -04:00
parent 613c4dfa8b
commit 3e73368eaa
2 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/AnomalyCancellation/LinearMaps.lean
View file

@ -41,7 +41,6 @@ lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a
end HomogeneousQuadratic
/-- The structure of a bilinear map. -/
structure BiLinear (V : Type) [AddCommMonoid V] [Module ℚ V] where
/-- The underling function. -/