smulCommClass — Mathlib

English

Given SMul M α, SMul N α, and SMulCommClass M N α, the pulled-back SMul on α via g: N → M yields SMulCommClass N α with respect to the second action.

Русский

Имея SMul M α, SMul N α и SMulCommClass M N α, тянущееся обратно SMul по g: N → M задаёт SMulCommClass N α.

LaTeX

$$$ [SMul M α],[SMul N α],[SMulCommClass M N α] \Rightarrow SMulCommClass N α, \; \text{через } g. $$$

Lean4

@[to_additive]
theorem smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N α] {f : α → β} (hf : Surjective f)
    (h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N β where
  smul_comm c₁ c₂ := hf.forall.2 fun x ↦ by simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

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