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

Update Basic.lean

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

2
HepLean/AnomalyCancellation/Basic.lean
View file

@ -87,7 +87,7 @@ lemma LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val)
simp_all only simp_all only
/-- An instance providing the operations and properties for `LinSols` to form an /-- An instance providing the operations and properties for `LinSols` to form an
addative commutative monoid. -/ additive commutative monoid. -/
@[simps!] @[simps!]
instance linSolsAddCommMonoid (χ : ACCSystemLinear) : instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
AddCommMonoid χ.LinSols where AddCommMonoid χ.LinSols where