Theorems · Definition · nonassociative algebras

NonUnitalAlgHom.inverse

{R : Type u} →
  [inst : Monoid R] →
    {A : Type v} →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : DistribMulAction R A] →
          {B₁ : Type u_2} →
            [inst_3 : NonUnitalNonAssocSemiring B₁] →
              [inst_4 : DistribMulAction R B₁] →
                (f : A →ₙₐ[R] B₁) → (g : B₁ → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B₁ →ₙₐ[R] A

The inverse of a bijective morphism is a morphism.

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulAction