inverse' — Mathlib

English

If an action is IsSMulRegular for N and f: F is injective, then the action is IsSMulRegular for M.

Русский

Если действие регуляторно для N и отображение инъективно, то действие регуляторно и для M.

LaTeX

$$IsSMulRegular M r$$

Lean4

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

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