Theorems · Definition · group theory

MulSemiringActionHom.inverse

{M : Type u_1} →
  [inst : Monoid M] →
    {R : Type u_10} →
      [inst_1 : Semiring R] →
        [inst_2 : MulSemiringAction M R] →
          {S₁ : Type u_15} →
            [inst_3 : Semiring S₁] →
              [inst_4 : MulSemiringAction M S₁] →
                (f : R →+*[M] S₁) → (g : S₁ → R) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S₁ →+*[M] R

The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

MonoidSemiringMulSemiringActionSemiringMulSemiringAction