Commit 2022-12-07 07:37 778daab3

View on Github →

feat port: GroupTheory.GroupAction.Option (#884) Mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996 This was also an easy one

Estimated changes

added theorem Option.smul_def
added theorem Option.smul_none
added theorem Option.smul_some