Registry · Theorem III.T39 tau-effective formalized

III.T39 — Enriched Bi-Square Comparison

The enriched bi-square has identical shape and structural maps as the algebraic (I.T41) and topological (II.T49) bi-squares

Book III Part 6 Ch. 50

Dependency Graph

Depends on (2)

III.D65 III.T38

Depended on by (1)

III.T40

Lean Formalization

Module: TauLib.BookIII.Arithmetic.EnrichedBiSquare

Symbol: bisquare_comparison_check