Group actions applied to various types of group #
This file contains lemmas about SMul on GroupWithZero, and Group.
instance
CancelMonoidWithZero.faithfulSMul
{α : Type u}
[CancelMonoidWithZero α]
[Nontrivial α]
:
FaithfulSMul α α
Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.
Equations
- ⋯ = ⋯
@[simp]
theorem
Commute.smul_right_iff₀
{α : Type u}
{β : Type v}
[GroupWithZero α]
[MulAction α β]
[Mul β]
[SMulCommClass α β β]
[IsScalarTower α β β]
{a : β}
{b : β}
{c : α}
(hc : c ≠ 0)
:
@[simp]
theorem
Commute.smul_left_iff₀
{α : Type u}
{β : Type v}
[GroupWithZero α]
[MulAction α β]
[Mul β]
[SMulCommClass α β β]
[IsScalarTower α β β]
{a : β}
{b : β}
{c : α}
(hc : c ≠ 0)
:
@[simp]
theorem
Equiv.smulRight_apply
{α : Type u}
{β : Type v}
[GroupWithZero α]
[MulAction α β]
{a : α}
(ha : a ≠ 0)
(b : β)
:
(Equiv.smulRight ha) b = a • b
@[simp]
theorem
Equiv.smulRight_symm_apply
{α : Type u}
{β : Type v}
[GroupWithZero α]
[MulAction α β]
{a : α}
(ha : a ≠ 0)
(b : β)
:
(Equiv.smulRight ha).symm b = a⁻¹ • b
def
Equiv.smulRight
{α : Type u}
{β : Type v}
[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 := ⋯ }
Instances For
def
DistribMulAction.toAddEquiv₀
{α : Type u_1}
(β : Type u_2)
[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 = let __src := DistribMulAction.toAddMonoidHom β x; { toFun := (↑__src).toFun, invFun := fun (b : β) => x⁻¹ • b, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }