domLCongr_trans — Mathlib

English

Composition of domain-congruences corresponds to domain-congruence of the composition of the domain equivalences.

Русский

Сложение согласований домена соответствует согласованию домена от композиции эквивалентностей домена.

LaTeX

$$$(\mathrm{domLCongr}\,f).\mathrm{trans}(\mathrm{domLCongr}\,f_2) = \mathrm{domLCongr}(f\,\mathrm{trans}\,f_2)$$$

Lean4

theorem domLCongr_trans {α₁ α₂ α₃ : Type*} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) :
    (Finsupp.domLCongr f).trans (Finsupp.domLCongr f₂) = (Finsupp.domLCongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _) :=
  LinearEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm

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