Theorems · Definition · group theory

MulDistribMulActionHom.inverse

{M : Type u_1} →
  [inst : Monoid M] →
    {A : Type u_4} →
      [inst_1 : Monoid A] →
        [inst_2 : MulDistribMulAction M A] →
          {B₁ : Type u_6} →
            [inst_3 : Monoid B₁] →
              [inst_4 : MulDistribMulAction 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 MulDistribMulActionHom is a MulDistribMulActionHom.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

MonoidMonoidMulDistribMulActionMonoidMulDistribMulAction