Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 19:03 ebf73435

View on Github →

feat(analysis/normed*): add instances and lemmas (#15515)

  • Add some coe_* lemmas.
  • Add is_scalar_tower and is_smul_class instances.

Estimated changes

modified theorem units.inv_unique
added theorem units.coe_div
added theorem coe_div_unit_sphere
added theorem coe_inv_unit_sphere
added theorem coe_mul_unit_ball
added theorem coe_mul_unit_sphere
added theorem coe_one_unit_sphere
added theorem coe_pow_unit_sphere
added theorem coe_zpow_unit_sphere