Commit 2022-12-06 23:44 ffc45d31

View on Github →

feat port: GroupTheory.GroupAction.Units (#878) Mathlib SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/Units.lean

added theorem IsUnit.inv_smul

added theorem IsUnit.smul

added theorem Units.smul_def

added theorem Units.smul_inv

added theorem Units.smul_is_unit

added theorem Units.val_smul