michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Change to dirsum_elim_compute

Browse source
This commit is contained in:
Robert Rose 2017-06-07 10:28:00 -06:00
parent 5fffcd6f70
commit 9256bf8861
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
algebra/direct_sum.hlean
View file

@ -73,10 +73,10 @@ namespace group
definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
dirsum_elim f ∘g dirsum_incl i ~ f i :=
definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) (y : Y i) :
dirsum_elim f (dirsum_incl i y) = f i y :=
begin
intro g, apply one_mul
apply one_mul
end
definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')