Commit 2022-12-07 07:59 70683c90

View on Github →

feat port: Group theory.GroupAction.Sum (#882) Mathlib SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996 This was an easy one

Estimated changes

added theorem Sum.smul_def
added theorem Sum.smul_inl
added theorem Sum.smul_inr
added theorem Sum.smul_swap