Commit 2023-05-25 17:58 c111a30b

View on Github →

feat: port Analysis.Complex.UnitDisc.Basic (#4180)

Estimated changes

Modified Mathlib.lean

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

added theorem Complex.UnitDisc.abs_lt_one

added theorem Complex.UnitDisc.abs_ne_one

added theorem Complex.UnitDisc.coe_conj

added theorem Complex.UnitDisc.coe_eq_zero

added theorem Complex.UnitDisc.coe_injective

added theorem Complex.UnitDisc.coe_mk

added theorem Complex.UnitDisc.coe_mul

added theorem Complex.UnitDisc.coe_ne_neg_one

added theorem Complex.UnitDisc.coe_ne_one

added theorem Complex.UnitDisc.coe_smul_circle

added theorem Complex.UnitDisc.coe_smul_closedBall

added theorem Complex.UnitDisc.coe_zero

added def Complex.UnitDisc.conj

added theorem Complex.UnitDisc.conj_conj

added theorem Complex.UnitDisc.conj_mul

added theorem Complex.UnitDisc.conj_neg

added theorem Complex.UnitDisc.conj_zero

added def Complex.UnitDisc.im

added theorem Complex.UnitDisc.im_coe

added theorem Complex.UnitDisc.im_conj

added theorem Complex.UnitDisc.im_neg

added def Complex.UnitDisc.mk

added theorem Complex.UnitDisc.mk_coe

added theorem Complex.UnitDisc.mk_neg

added theorem Complex.UnitDisc.normSq_lt_one

added theorem Complex.UnitDisc.one_add_coe_ne_zero

added def Complex.UnitDisc.re

added theorem Complex.UnitDisc.re_coe

added theorem Complex.UnitDisc.re_conj

added theorem Complex.UnitDisc.re_neg

added def Complex.UnitDisc