Theorems · Theorem · group theory

MulSemiringActionHom.inverse_toFun

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

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext

Assumes

MonoidSemiringMulSemiringActionSemiringMulSemiringAction