domDomCongr_smul — Mathlib

English

Transitivity of domDomCongr with respect to composition of equivalences.

Русский

Транзитивность domDomCongr по отношению к композиции эквивалентностей.

LaTeX

$$domDomCongr_trans (σ1) (σ2) (f) = (domDomCongr σ2).domDomCongr σ1 f$$

Lean4

@[simp]
theorem domDomCongr_smul {S : Type*} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (σ : ι ≃ ι') (c : S)
    (f : M [⋀^ι]→ₗ[R] N) : (c • f).domDomCongr σ = c • f.domDomCongr σ :=
  rfl

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