Commit 2022-12-07 23:03 b4b59ba6

View on Github →

feat port: GroupTheory.GroupAction.Sigma (#885) mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996 Another easy one.

Estimated changes

added theorem Sigma.smul_def
added theorem Sigma.smul_mk