Commit 2026-01-07 06:27 18978c91

View on Github →

chore(UnitDisc): review API (#33639)

Define a Star instance instead of UnitDisc.conj.
Move the notation from the _root_.UnitDisc scope to Complex.UnitDisc.
Define casesOn.
Add inst to instance names. Cherry-picked from #33368

Estimated changes

Modified Mathlib/Analysis/Complex/UnitDisc/Basic.lean

added theorem Complex.UnitDisc.casesOn_mk

added theorem Complex.UnitDisc.coe_circle_smul

added theorem Complex.UnitDisc.coe_closedBall_smul

deleted theorem Complex.UnitDisc.coe_conj

added theorem Complex.UnitDisc.coe_neg

deleted theorem Complex.UnitDisc.coe_smul_circle

deleted theorem Complex.UnitDisc.coe_smul_closedBall

added theorem Complex.UnitDisc.coe_star

deleted def Complex.UnitDisc.conj

modified theorem Complex.UnitDisc.conj_conj

modified theorem Complex.UnitDisc.conj_mul

deleted theorem Complex.UnitDisc.conj_neg

deleted theorem Complex.UnitDisc.conj_zero

deleted theorem Complex.UnitDisc.im_conj

deleted theorem Complex.UnitDisc.re_conj

added theorem Complex.UnitDisc.sq_norm_lt_one