chain_linearPMap_of_chain_extensionOf

English

There is a biadditive monoid homomorphism smul: R →+ M →+ M, giving a bilinear action of R on the additive monoid M whenever M is a module over R.

Русский

Существует биаддитивное отображение smul: R →+ M →+ M, задающее биаддитивное действие R на M при условии, что M — модуль над R.

LaTeX

$$$ \text{smul} : R \to^+ M \to^+ M$$$

Lean4

theorem chain_linearPMap_of_chain_extensionOf {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c) :
    IsChain (· ≤ ·) <| (fun x : ExtensionOf i f => x.toLinearPMap) '' c :=
  by
  rintro _ ⟨a, a_mem, rfl⟩ _ ⟨b, b_mem, rfl⟩ neq
  exact hchain a_mem b_mem (ne_of_apply_ne _ neq)

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