cau_seq{_completion}): add lemmas about pow and smul (#17796)

Commit

3 years ago

chore(data/real/cau_seq{_completion}): add lemmas about pow and smul (#17796) This also takes the opportunity to golf the algebraic instances, which should make porting easier.

Author

eric-wieser

Parents

6c48d300

mathlib3 dce07aeb - chore(data/real/cau_seq{_completion}): add lemmas about pow and smul (#17796)

mathlib3
dce07aeb - chore(data/real/cau_seq{_completion}): add lemmas about pow and smul (#17796)