Registry · Definition II.D85 tau-effective formalized

II.D85 — Homology via SES

Homology via short exact sequences: 0 → Z/M_{k-1} → Z/M_k → Z/p_k → 0. Exactness at the middle: ker(g) = im(f), giving trivial homology H = 0.

Book II Part 8 Ch. 46

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookII.Enrichment.Homological

Symbol: ses_exactness_check