Multiplicative actions with zero on and by Mˣ

This file provides the multiplicative actions with zero of a unit on a type α, SMul Mˣ α, in the presence of SMulWithZero M α, with the obvious definition stated in Units.smul_def.

Additionally, a MulDistribMulAction G M for some group G satisfying some additional properties admits a MulDistribMulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul. This instance uses a primed name.

See also

• Algebra.GroupWithZero.Action.Opposite
• Algebra.GroupWithZero.Action.Pi
• Algebra.GroupWithZero.Action.Prod

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Commute.smul_right_iff₀ {α : Type u_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (Equiv.smulRight ha).symm b = a⁻¹ • b

@[simp]

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

def Equiv.smulRight {α : Type u_3} {β : Type u_4} [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 := ⋯ }

Action of the units of M on a type α

instance AddUnits.instVAdd_1 {M : Type u_2} {α : Type u_3} [AddMonoid M] [VAdd M α] : VAdd (AddUnits M) α

Equations

• AddUnits.instVAdd_1 = { vadd := fun (m : AddUnits M) (a : α) => ↑m +ᵥ a }

instance Units.instSMul_1 {M : Type u_2} {α : Type u_3} [Monoid M] [SMul M α] : SMul Mˣ α

Equations

• Units.instSMul_1 = { smul := fun (m : Mˣ) (a : α) => ↑m • a }

instance Units.instSMulZeroClass {M : Type u_2} {α : Type u_3} [Monoid M] [Zero α] [SMulZeroClass M α] : SMulZeroClass Mˣ α

Equations

• Units.instSMulZeroClass = SMulZeroClass.mk ⋯

instance Units.instDistribSMulUnits {M : Type u_2} {α : Type u_3} [Monoid M] [AddZeroClass α] [DistribSMul M α] : DistribSMul Mˣ α

Equations

• Units.instDistribSMulUnits = DistribSMul.mk ⋯

instance Units.instDistribMulAction {M : Type u_2} {α : Type u_3} [Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction Mˣ α

Equations

• Units.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

instance Units.instMulDistribMulAction {M : Type u_2} {α : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction Mˣ α

Equations

• Units.instMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

Action of a group G on units of M

instance Units.mulDistribMulAction' {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] [MulDistribMulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : MulDistribMulAction G Mˣ

A stronger form of Units.mul_action'.

Equations

• Units.mulDistribMulAction' = MulDistribMulAction.mk ⋯ ⋯

@[simp]

theorem IsUnit.smul_eq_zero {G : Type u_1} {M : Type u_2} [Monoid G] [AddMonoid M] [DistribMulAction G M] {u : G} {x : M} (hu : IsUnit u) : u • x = 0 ↔ x = 0