inverse — Mathlib

English

The inverse of a bijective MulSemiringActionHom is again a MulSemiringActionHom (construction with the inverse map).

Русский

Обратный биективного MulSemiringActionHom снова является MulSemiringActionHom (конструкция через обратную карту).

LaTeX

$$inverse : MulSemiringActionHom φ R S → S → R$$

Lean4

/-- The inverse of a bijective `MulSemiringActionHom` is a `MulSemiringActionHom`. -/
@[simps]
def inverse {S₁ : Type*} [Semiring S₁] [MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁ → R)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S₁ →+*[M] R :=
  { (f : R →+ S₁).inverse g h₁ h₂, (f : R →* S₁).inverse g h₁ h₂, f.toMulActionHom.inverse g h₁ h₂ with toFun := g }

Похожие утверждения