Registry · Proposition II.P14 established formalized

II.P14 — Character Algebra Ring Structure

Character Algebra Ring Structure

Book II Part 9 Ch. 47

Dependency Graph

Depends on (2)

II.D59 I.D21

Lean Formalization

Module: TauLib.BookII.CentralTheorem.BoundaryCharacters

Symbol: Tau.BookII.CentralTheorem.character_add_check