dvd_smul_of_dvd — Mathlib

English

Let M act on a semigroup R with a commuting action. If x ∣ y in R, then for any m ∈ M, x ∣ m • y.

Русский

Пусть M действует на полугруппа R так, чтобы действие коммутировало. Если x делится на y в R, то для любого m ∈ M выполняется x | m • y.

LaTeX

$$$x \mid y \Rightarrow x \mid m \cdot y$$$

Lean4

theorem dvd_smul_of_dvd {M : Type*} [SMul M R] [Semigroup R] [SMulCommClass M R R] {x y : R} (m : M) (h : x ∣ y) :
    x ∣ m • y :=
  let ⟨k, hk⟩ := h;
  ⟨m • k, by rw [mul_smul_comm, ← hk]⟩

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