Theorems · Theorem · nonassociative algebras

NonUnitalAlgHom.coe_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) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), ⇑(f.inverse g h₁ h₂) = g

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulAction