Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-16 08:11 6188b991

View on Github →

feat(topology/instances/ennreal): more lemmas about tsum (#1756)

  • feat(data/real/ennreal): more lemmas, *_cast tags, use lift tactic
  • Undo name change
  • Fix compile
  • nnreal: add move_cast
  • ennreal: more lemmas
  • Fix compile
  • feat(topology/instances/ennreal): more lemmas
  • Fix compile

Estimated changes

modified theorem ennreal.tendsto_coe