Definitions of group actions

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

• MulAction M α and its additive version AddAction G P are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classes SMul and VAdd that are defined in Algebra.Group.Defs;
• DistribMulAction M A is a typeclass for an action of a multiplicative monoid on an additive monoid such that a • (b + c) = a • b + a • c and a • 0 = 0.

The hierarchy is extended further by Module, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

• SMulCommClass M N α and its additive version VAddCommClass M N α;
• IsScalarTower M N α and its additive version VAddAssocClass M N α;
• IsCentralScalar M α and its additive version IsCentralVAdd M N α.

Notation

• a • b is used as notation for SMul.smul a b.
• a +ᵥ b is used as notation for VAdd.vadd a b.

Implementation details

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags

group action

instance CancelMonoidWithZero.faithfulSMul {α : Type u_9} [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul α α

Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.

Equations

• ⋯ = ⋯

@[simp]

theorem inv_smul_smul₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x

@[simp]

theorem smul_inv_smul₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x

theorem inv_smul_eq_iff₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x : β} {y : β} : a⁻¹ • x = y ↔ x = a • y

theorem eq_inv_smul_iff₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x : β} {y : β} : x = a⁻¹ • y ↔ a • x = y

@[simp]

theorem Commute.smul_right_iff₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x : β} {y : β} (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y

@[simp]

theorem Commute.smul_left_iff₀ {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x : β} {y : β} (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y

@[simp]

theorem Equiv.smulRight_symm_apply {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (Equiv.smulRight ha).symm b = a⁻¹ • b

@[simp]

theorem Equiv.smulRight_apply {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (Equiv.smulRight ha) b = a • b

def Equiv.smulRight {α : Type u_9} {β : Type u_10} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : β ≃ β

Right scalar multiplication as an order isomorphism.

Equations

• Equiv.smulRight ha = { toFun := fun (b : β) => a • b, invFun := fun (b : β) => a⁻¹ • b, left_inv := ⋯, right_inv := ⋯ }

class SMulZeroClass (M : Type u_11) (A : Type u_12) [Zero A] extends SMul : Type (max u_11 u_12)

Typeclass for scalar multiplication that preserves 0 on the right.

• smul : M → A → A
• smul_zero : ∀ (a : M), a • 0 = 0

  Multiplying 0 by a scalar gives 0

theorem SMulZeroClass.smul_zero {M : Type u_11} {A : Type u_12} [Zero A] [self : SMulZeroClass M A] (a : M) : a • 0 = 0

Multiplying 0 by a scalar gives 0

@[simp]

theorem smul_zero {M : Type u_3} {A : Type u_7} [Zero A] [SMulZeroClass M A] (a : M) : a • 0 = 0

theorem smul_ite_zero {M : Type u_3} {A : Type u_7} [Zero A] [SMulZeroClass M A] (p : Prop) [Decidable p] (a : M) (b : A) : (a • if p then b else 0) = if p then a • b else 0

theorem smul_eq_zero_of_right {M : Type u_3} {A : Type u_7} [Zero A] [SMulZeroClass M A] (a : M) {b : A} (h : b = 0) : a • b = 0

theorem right_ne_zero_of_smul {M : Type u_3} {A : Type u_7} [Zero A] [SMulZeroClass M A] {a : M} {b : A} : a • b ≠ 0 → b ≠ 0

@[reducible, inline]

abbrev Function.Injective.smulZeroClass {M : Type u_3} {A : Type u_7} {B : Type u_8} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom B A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : SMulZeroClass M B

Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].

Equations

• Function.Injective.smulZeroClass f hf smul = SMulZeroClass.mk ⋯

@[reducible, inline]

abbrev ZeroHom.smulZeroClass {M : Type u_3} {A : Type u_7} {B : Type u_8} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : SMulZeroClass M B

Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].

Equations

• f.smulZeroClass smul = SMulZeroClass.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.smulZeroClassLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [Zero M] [SMulZeroClass R M] [SMul S M] (f : R → S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : SMulZeroClass S M

Push forward the multiplication of R on M along a compatible surjective map f : R → S.

See also Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.smulZeroClassLeft f hf hsmul = SMulZeroClass.mk ⋯

@[reducible, inline]

abbrev SMulZeroClass.compFun {M : Type u_3} {N : Type u_5} (A : Type u_7) [Zero A] [SMulZeroClass M A] (f : N → M) : SMulZeroClass N A

Compose a SMulZeroClass with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

Equations

• SMulZeroClass.compFun A f = SMulZeroClass.mk ⋯

@[simp]

theorem SMulZeroClass.toZeroHom_apply {M : Type u_3} (A : Type u_7) [Zero A] [SMulZeroClass M A] (x : M) : ∀ (x_1 : A), (SMulZeroClass.toZeroHom A x) x_1 = x • x_1

def SMulZeroClass.toZeroHom {M : Type u_3} (A : Type u_7) [Zero A] [SMulZeroClass M A] (x : M) : ZeroHom A A

Each element of the scalars defines a zero-preserving map.

Equations

• SMulZeroClass.toZeroHom A x = { toFun := fun (x_1 : A) => x • x_1, map_zero' := ⋯ }

theorem DistribSMul.ext_iff {M : Type u_11} {A : Type u_12} : ∀ {inst : AddZeroClass A} {x y : DistribSMul M A}, x = y ↔ SMul.smul = SMul.smul

theorem DistribSMul.ext {M : Type u_11} {A : Type u_12} : ∀ {inst : AddZeroClass A} {x y : DistribSMul M A}, SMul.smul = SMul.smul → x = y

class DistribSMul (M : Type u_11) (A : Type u_12) [AddZeroClass A] extends SMulZeroClass : Type (max u_11 u_12)

Typeclass for scalar multiplication that preserves 0 and + on the right.

This is exactly DistribMulAction without the MulAction part.

• smul : M → A → A
• smul_zero : ∀ (a : M), a • 0 = 0
• smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

theorem DistribSMul.smul_add {M : Type u_11} {A : Type u_12} [AddZeroClass A] [self : DistribSMul M A] (a : M) (x : A) (y : A) : a • (x + y) = a • x + a • y

Scalar multiplication distributes across addition

theorem smul_add {M : Type u_3} {A : Type u_7} [AddZeroClass A] [DistribSMul M A] (a : M) (b₁ : A) (b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂

instance AddMonoidHom.smulZeroClass {M : Type u_3} {A : Type u_7} {B : Type u_8} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] : SMulZeroClass M (B →+ A)

Equations

• AddMonoidHom.smulZeroClass = SMulZeroClass.mk ⋯

@[reducible, inline]

abbrev Function.Injective.distribSMul {M : Type u_3} {A : Type u_7} {B : Type u_8} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : B →+ A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribSMul M B

Pullback a distributive scalar multiplication along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.distribSMul f hf smul = DistribSMul.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.distribSMul {M : Type u_3} {A : Type u_7} {B : Type u_8} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : A →+ B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribSMul M B

Pushforward a distributive scalar multiplication along a surjective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Surjective.distribSMul f hf smul = DistribSMul.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.distribSMulLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : R → S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribSMul S M

Push forward the multiplication of R on M along a compatible surjective map f : R → S.

See also Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.distribSMulLeft f hf hsmul = DistribSMul.mk ⋯

@[reducible, inline]

abbrev DistribSMul.compFun {M : Type u_3} {N : Type u_5} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (f : N → M) : DistribSMul N A

Compose a DistribSMul with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

Equations

• DistribSMul.compFun A f = DistribSMul.mk ⋯

@[simp]

theorem DistribSMul.toAddMonoidHom_apply {M : Type u_3} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (x : M) : ∀ (x2 : A), (DistribSMul.toAddMonoidHom A x) x2 = (fun (x1 : M) (x2 : A) => x1 • x2) x x2

def DistribSMul.toAddMonoidHom {M : Type u_3} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (x : M) : A →+ A

Each element of the scalars defines an additive monoid homomorphism.

Equations

• DistribSMul.toAddMonoidHom A x = { toFun := (fun (x1 : M) (x2 : A) => x1 • x2) x, map_zero' := ⋯, map_add' := ⋯ }

theorem DistribMulAction.ext_iff {M : Type u_11} {A : Type u_12} : ∀ {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A}, x = y ↔ SMul.smul = SMul.smul

theorem DistribMulAction.ext {M : Type u_11} {A : Type u_12} : ∀ {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A}, SMul.smul = SMul.smul → x = y

class DistribMulAction (M : Type u_11) (A : Type u_12) [Monoid M] [AddMonoid A] extends MulAction : Type (max u_11 u_12)

Typeclass for multiplicative actions on additive structures. This generalizes group modules.

• smul : M → A → A
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : M) (b : A), (x * y) • b = x • y • b
• smul_zero : ∀ (a : M), a • 0 = 0

  Multiplying 0 by a scalar gives 0

• smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

theorem DistribMulAction.smul_zero {M : Type u_11} {A : Type u_12} [Monoid M] [AddMonoid A] [self : DistribMulAction M A] (a : M) : a • 0 = 0

Multiplying 0 by a scalar gives 0

theorem DistribMulAction.smul_add {M : Type u_11} {A : Type u_12} [Monoid M] [AddMonoid A] [self : DistribMulAction M A] (a : M) (x : A) (y : A) : a • (x + y) = a • x + a • y

Scalar multiplication distributes across addition

@[instance 100]

instance DistribMulAction.toDistribSMul {M : Type u_3} {A : Type u_7} [Monoid M] [AddMonoid A] [DistribMulAction M A] : DistribSMul M A

Equations

• DistribMulAction.toDistribSMul = DistribSMul.mk ⋯

Since Lean 3 does not have definitional eta for structures, we have to make sure that the definition of DistribMulAction.toDistribSMul was done correctly, and the two paths from DistribMulAction to SMul are indeed definitionally equal.

@[reducible, inline]

abbrev Function.Injective.distribMulAction {M : Type u_3} {A : Type u_7} {B : Type u_8} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : B →+ A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribMulAction M B

Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.distribMulAction f hf smul = DistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.distribMulAction {M : Type u_3} {A : Type u_7} {B : Type u_8} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribMulAction M B

Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Surjective.distribMulAction f hf smul = DistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.distribMulActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribMulAction S M

Push forward the action of R on M along a compatible surjective map f : R →* S.

See also Function.Surjective.mulActionLeft and Function.Surjective.moduleLeft.

Equations

• Function.Surjective.distribMulActionLeft f hf hsmul = DistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev DistribMulAction.compHom {M : Type u_3} {N : Type u_5} (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] [Monoid N] (f : N →* M) : DistribMulAction N A

Compose a DistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Equations

• DistribMulAction.compHom A f = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_3} (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : ∀ (x2 : A), (DistribMulAction.toAddMonoidHom A x) x2 = x • x2

def DistribMulAction.toAddMonoidHom {M : Type u_3} (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : A →+ A

Each element of the monoid defines an additive monoid homomorphism.

Equations

• DistribMulAction.toAddMonoidHom A x = DistribSMul.toAddMonoidHom A x

@[simp]

theorem DistribMulAction.toAddMonoidEnd_apply (M : Type u_3) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : (DistribMulAction.toAddMonoidEnd M A) x = DistribMulAction.toAddMonoidHom A x

def DistribMulAction.toAddMonoidEnd (M : Type u_3) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : M →* AddMonoid.End A

Each element of the monoid defines an additive monoid homomorphism.

Equations

• DistribMulAction.toAddMonoidEnd M A = { toFun := DistribMulAction.toAddMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }

instance AddMonoid.nat_smulCommClass (M : Type u_3) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass ℕ M A

Equations

• ⋯ = ⋯

instance AddMonoid.nat_smulCommClass' (M : Type u_3) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass M ℕ A

Equations

• ⋯ = ⋯

instance AddGroup.int_smulCommClass {M : Type u_3} {A : Type u_7} [Monoid M] [AddGroup A] [DistribMulAction M A] : SMulCommClass ℤ M A

Equations

• ⋯ = ⋯

instance AddGroup.int_smulCommClass' {M : Type u_3} {A : Type u_7} [Monoid M] [AddGroup A] [DistribMulAction M A] : SMulCommClass M ℤ A

Equations

• ⋯ = ⋯

@[simp]

theorem smul_neg {M : Type u_3} {A : Type u_7} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) : r • -x = -(r • x)

theorem smul_sub {M : Type u_3} {A : Type u_7} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) (y : A) : r • (x - y) = r • x - r • y

theorem MulDistribMulAction.ext {M : Type u_11} {A : Type u_12} : ∀ {inst : Monoid M} {inst_1 : Monoid A} {x y : MulDistribMulAction M A}, SMul.smul = SMul.smul → x = y

theorem MulDistribMulAction.ext_iff {M : Type u_11} {A : Type u_12} : ∀ {inst : Monoid M} {inst_1 : Monoid A} {x y : MulDistribMulAction M A}, x = y ↔ SMul.smul = SMul.smul

class MulDistribMulAction (M : Type u_11) (A : Type u_12) [Monoid M] [Monoid A] extends MulAction : Type (max u_11 u_12)

Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.

• smul : M → A → A
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : M) (b : A), (x * y) • b = x • y • b
• smul_mul : ∀ (r : M) (x y : A), r • (x * y) = r • x * r • y

  Distributivity of • across *

• smul_one : ∀ (r : M), r • 1 = 1

  Multiplying 1 by a scalar gives 1

theorem MulDistribMulAction.smul_mul {M : Type u_11} {A : Type u_12} [Monoid M] [Monoid A] [self : MulDistribMulAction M A] (r : M) (x : A) (y : A) : r • (x * y) = r • x * r • y

Distributivity of • across *

theorem MulDistribMulAction.smul_one {M : Type u_11} {A : Type u_12} [Monoid M] [Monoid A] [self : MulDistribMulAction M A] (r : M) : r • 1 = 1

Multiplying 1 by a scalar gives 1

theorem smul_mul' {M : Type u_3} {A : Type u_7} [Monoid M] [Monoid A] [MulDistribMulAction M A] (a : M) (b₁ : A) (b₂ : A) : a • (b₁ * b₂) = a • b₁ * a • b₂

@[reducible, inline]

abbrev Function.Injective.mulDistribMulAction {M : Type u_3} {A : Type u_7} {B : Type u_8} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : B →* A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : MulDistribMulAction M B

Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.mulDistribMulAction f hf smul = MulDistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.mulDistribMulAction {M : Type u_3} {A : Type u_7} {B : Type u_8} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : A →* B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : MulDistribMulAction M B

Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Surjective.mulDistribMulAction f hf smul = MulDistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev MulDistribMulAction.compHom {M : Type u_3} {N : Type u_5} (A : Type u_7) [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid N] (f : N →* M) : MulDistribMulAction N A

Compose a MulDistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Equations

• MulDistribMulAction.compHom A f = MulDistribMulAction.mk ⋯ ⋯

def MulDistribMulAction.toMonoidHom {M : Type u_3} (A : Type u_7) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) : A →* A

Scalar multiplication by r as a MonoidHom.

Equations

• MulDistribMulAction.toMonoidHom A r = { toFun := fun (x : A) => r • x, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_3} {A : Type u_7} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) : (MulDistribMulAction.toMonoidHom A r) x = r • x

@[simp]

theorem smul_pow' {M : Type u_3} {A : Type u_7} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n

@[simp]

theorem MulDistribMulAction.toMonoidEnd_apply (M : Type u_3) (A : Type u_7) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) : (MulDistribMulAction.toMonoidEnd M A) r = MulDistribMulAction.toMonoidHom A r

def MulDistribMulAction.toMonoidEnd (M : Type u_3) (A : Type u_7) [Monoid M] [Monoid A] [MulDistribMulAction M A] : M →* Monoid.End A

Each element of the monoid defines a monoid homomorphism.

Equations

• MulDistribMulAction.toMonoidEnd M A = { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem smul_inv' {M : Type u_3} {A : Type u_7} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) : r • x⁻¹ = (r • x)⁻¹

theorem smul_div' {M : Type u_3} {A : Type u_7} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) (y : A) : r • (x / y) = r • x / r • y

instance AddMonoid.End.applyDistribMulAction {α : Type u_9} [AddMonoid α] : DistribMulAction (AddMonoid.End α) α

The tautological action by AddMonoid.End α on α.

This generalizes Function.End.applyMulAction.

Equations

• AddMonoid.End.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem AddMonoid.End.smul_def {α : Type u_9} [AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a

instance AddMonoid.End.applyFaithfulSMul {α : Type u_9} [AddMonoid α] : FaithfulSMul (AddMonoid.End α) α

AddMonoid.End.applyDistribMulAction is faithful.

Equations

• ⋯ = ⋯

def DistribMulAction.toAddEquiv₀ {α : Type u_11} (β : Type u_12) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β

Each non-zero element of a GroupWithZero defines an additive monoid isomorphism of an AddMonoid on which it acts distributively. This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations

• DistribMulAction.toAddEquiv₀ β x hx = { toFun := (↑(DistribMulAction.toAddMonoidHom β x)).toFun, invFun := fun (b : β) => x⁻¹ • b, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem smul_eq_zero_iff_eq {α : Type u_9} {β : Type u_10} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_ne {α : Type u_9} {β : Type u_10} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0