Commit 2022-12-22 16:23 e0d4c040

View on Github →

feat port: GroupTheory.GroupAction.Group (#1146)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

Created Mathlib/GroupTheory/GroupAction/Group.lean

added def AddAction.toPermHom

added theorem Commute.smul_left_iff

added theorem Commute.smul_left_iff₀

added theorem Commute.smul_right_iff

added theorem Commute.smul_right_iff₀

added def DistribMulAction.toAddAut

added def DistribMulAction.toAddEquiv

added theorem IsUnit.smul_eq_zero

added theorem IsUnit.smul_left_cancel

added theorem IsUnit.smul_sub_iff_sub_inv_smul

added def MulAction.toPerm

added def MulAction.toPermHom

added theorem MulAction.to_perm_injective

added def MulDistribMulAction.toMulAut

added def MulDistribMulAction.toMulEquiv

added def arrowAction

added def arrowMulDistribMulAction

added theorem eq_inv_smul_iff

added theorem eq_inv_smul_iff₀

added theorem inv_smul_eq_iff

added theorem inv_smul_eq_iff₀

added theorem inv_smul_smul

added theorem inv_smul_smul₀

added theorem is_unit_smul_iff

added def mulAutArrow

added theorem smul_eq_iff_eq_inv_smul

added theorem smul_eq_zero_iff_eq'

added theorem smul_eq_zero_iff_eq

added theorem smul_inv

added theorem smul_inv_smul

added theorem smul_inv_smul₀

added theorem smul_left_cancel

added theorem smul_left_cancel_iff

added theorem smul_ne_zero_iff_ne'

added theorem smul_ne_zero_iff_ne

added theorem smul_zpow