Theorems · Definition · group theory

DistribMulActionHom.inverse

{M : Type u_1} →
  [inst : Monoid M] →
    {A : Type u_4} →
      [inst_1 : AddMonoid A] →
        [inst_2 : DistribMulAction M A] →
          {B₁ : Type u_6} →
            [inst_3 : AddMonoid B₁] →
              [inst_4 : DistribMulAction M B₁] →
                (f : A →+[M] B₁) → (g : B₁ → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B₁ →+[M] A

The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

MonoidAddMonoidDistribMulActionAddMonoidDistribMulAction