domDomCongrₗ_refl — Mathlib

English

If σ is the identity on ι, then the induced linear equivalence domDomCongr_ℓ is the identity on the space of alternating maps.

Русский

Если σ является тождественным на ι, то порожденное линейное эквалентное отображение domDomCongr_ℓ равно тождественному на пространстве чередующихся отображений.

LaTeX

$$$\\operatorname{domDomCongr}_{\\ell}(\\mathrm{refl}\\, ι) = \\mathrm{LinearEquiv.refl}.$$$

Lean4

@[simp]
theorem domDomCongrₗ_refl :
    (domDomCongrₗ S (Equiv.refl ι) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) = LinearEquiv.refl _ _ :=
  rfl

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