Commit 2025-04-19 07:26 121243ab

View on Github →

chore(Normed/Field/UnitBall): review instances (#24188)

Estimated changes

Modified Mathlib/Analysis/Complex/Circle.lean

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

added theorem Complex.UnitDisc.coe_inj

added theorem Complex.UnitDisc.mk_eq_zero

added theorem Complex.UnitDisc.mk_zero

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/Analysis/Normed/Field/UnitBall.lean

added theorem Metric.unitSphere.coe_inv

added theorem Metric.unitSphere.coe_mul

added theorem Metric.unitSphere.coe_pow

added theorem Metric.unitSphere.coe_zpow

deleted theorem coe_div_unitSphere

deleted theorem coe_inv_unitSphere

deleted theorem coe_mul_unitBall

deleted theorem coe_mul_unitClosedBall

deleted theorem coe_mul_unitSphere

deleted theorem coe_one_unitClosedBall

deleted theorem coe_one_unitSphere

deleted theorem coe_pow_unitClosedBall

deleted theorem coe_pow_unitSphere

deleted theorem coe_zpow_unitSphere