Registry · Definition II.D33 established formalized

II.D33 — Bipolar Idempotents Interior

Bipolar Idempotents Interior

Book II Part 5 Ch. 27

Dependency Graph

Depends on (2)

II.D32 I.D20

Depended on by (9)

II.D36 II.L02 II.L03 II.L04 II.P07 II.R10 II.T24 II.T26 II.T27

Lean Formalization

Module: TauLib.BookII.Transcendentals.JReplacesI

Symbol: j_exponential