smul — Mathlib

English

If c is a congruence on M and a acts on M, then c is stable under scalar action: a • w and a • x are related by c whenever w and x are related by c.

Русский

Если c — конгруэнция на M и элемент a действует на M, то подмножество сохраняется под действием скаляра: если w ∼ x под c, то a • w ∼ a • x.

LaTeX

$$c (a • w) (a • x)$$

Lean4

@[to_additive]
theorem smul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) {w x : M} (h : c w x) :
    c (a • w) (a • x) := by simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h

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