domLCongr_symm — Mathlib

English

The inverse of the domain-congruence induced by a bijection f is the domain-congruence induced by the inverse bijection f.symm.

Русский

Обратное согласование домена, полученное из биекции f, равно согласованию домена, полученному из ее обратной биекции.

LaTeX

$$$(\mathrm{domLCongr}\,f).symm = \mathrm{domLCongr}\,f^{-1}$$$

Lean4

@[simp]
theorem domLCongr_symm {α₁ α₂ : Type*} (f : α₁ ≃ α₂) :
    ((Finsupp.domLCongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLCongr f.symm :=
  LinearEquiv.ext fun _ => rfl

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