Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-28 14:32 8792402d

View on Github →

feat(analysis/complex): define complex.unit_disc (#17119)

Estimated changes

Created src/analysis/complex/unit_disc/basic.lean

added theorem complex.unit_disc.abs_lt_one

added theorem complex.unit_disc.abs_ne_one

added theorem complex.unit_disc.coe_conj

added theorem complex.unit_disc.coe_eq_zero

added theorem complex.unit_disc.coe_injective

added theorem complex.unit_disc.coe_mk

added theorem complex.unit_disc.coe_mul

added theorem complex.unit_disc.coe_ne_neg_one

added theorem complex.unit_disc.coe_ne_one

added theorem complex.unit_disc.coe_smul_circle

added theorem complex.unit_disc.coe_smul_closed_ball

added theorem complex.unit_disc.coe_zero

added def complex.unit_disc.conj

added theorem complex.unit_disc.conj_conj

added theorem complex.unit_disc.conj_mul

added theorem complex.unit_disc.conj_neg

added theorem complex.unit_disc.conj_zero

added def complex.unit_disc.im

added theorem complex.unit_disc.im_coe

added theorem complex.unit_disc.im_conj

added theorem complex.unit_disc.im_neg

added def complex.unit_disc.mk

added theorem complex.unit_disc.mk_coe

added theorem complex.unit_disc.mk_neg

added theorem complex.unit_disc.norm_sq_lt_one

added theorem complex.unit_disc.one_add_coe_ne_zero

added def complex.unit_disc.re

added theorem complex.unit_disc.re_coe

added theorem complex.unit_disc.re_conj

added theorem complex.unit_disc.re_neg

added def complex.unit_disc