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

fix typo

Browse source
This commit is contained in:
Jeremy Avigad 2017-03-02 17:08:00 -05:00
parent 89d65b1dca
commit e7c174719b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
algebra/is_short_exact.hlean
View file

@ -19,4 +19,4 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C)
(is_emb : is_embedding f) (is_emb : is_embedding f)
(im_in_ker : Π(a:A), g (f a) = pt) (im_in_ker : Π(a:A), g (f a) = pt)
(ker_in_im : Π(b:B), (g b = pt) → fiber f b) (ker_in_im : Π(b:B), (g b = pt) → fiber f b)
is_surj : is_split_surjective g) (is_surj : is_split_surjective g)