Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-01 10:44 3ede6d9e

View on Github →

feat(data/real/cau_seq): Make power elementwise (#17124) Redefine nsmul, zsmul, pow elementwise on Cauchy sequences. This gives a few lemmas for free (as they're now refl). Add some forgotten coe and const lemmas and tag some more with norm_cast.

Estimated changes

modified theorem cau_seq.add_apply
added theorem cau_seq.coe_add
added theorem cau_seq.coe_const
added theorem cau_seq.coe_inv
added theorem cau_seq.coe_mul
added theorem cau_seq.coe_neg
added theorem cau_seq.coe_one
added theorem cau_seq.coe_pow
added theorem cau_seq.coe_smul
added theorem cau_seq.coe_sub
added theorem cau_seq.coe_zero
modified theorem cau_seq.const_apply
modified theorem cau_seq.const_mul
modified theorem cau_seq.const_neg
added theorem cau_seq.const_one
added theorem cau_seq.const_pow
added theorem cau_seq.const_smul
modified theorem cau_seq.const_sub
modified theorem cau_seq.const_zero
modified theorem cau_seq.inv_apply
modified theorem cau_seq.mul_apply
modified theorem cau_seq.neg_apply
modified theorem cau_seq.one_apply
added theorem cau_seq.pow_apply
added theorem cau_seq.smul_apply
modified theorem cau_seq.sub_apply
modified theorem cau_seq.zero_apply
added theorem is_cau_seq.add