Registry · Proposition II.P19 tau-effective formalized

II.P19 — Long Exact Sequence

Short exact sequence of primorial quotients induces a long exact sequence in homology via the snake lemma. Connecting homomorphism δ exists.

Book II Part 8 Ch. 46

Dependency Graph

Depends on (2)

II.D85 II.T54

Lean Formalization

Module: TauLib.BookII.Enrichment.Homological

Symbol: les_stage2