Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.lim_mul_lim

Modification history

2018-11-05 17:46

data/real/basic.lean

refactor(cau_seq): unify real.lim, complex.lim and cau_seq.lim (#433)

Deleted real.lim_mul_lim View on Github →

2018-10-02 14:08

data/real/basic.lean

feat(data/padics): use prime typeclass

Modified real.lim_mul_lim View on Github →

2018-08-28 10:22

data/real/basic.lean

feat(data/real): cauchy sequence limit lemmas (#61)

Added real.lim_mul_lim View on Github →