toAddEquiv₀

Mathlib.Algebra.GroupWithZero.Action.End

URI: https://scilib.ai/kg/mathlib#DistribMulAction.toAddEquiv₀

Lean4

/-- 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`. -/
def toAddEquiv₀ {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x ≠ 0) :
    β ≃+ β :=
  { DistribMulAction.toAddMonoidHom β x with
    invFun := fun b ↦ x⁻¹ • b
    left_inv := fun b ↦ inv_smul_smul₀ hx b
    right_inv := fun b ↦ smul_inv_smul₀ hx b }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru