mk_coe' — Mathlib

English

Given data f,h1,h2,h3,h4 and an isomorphism e, the explicitly constructed linear equivalence equals e.symm.

Русский

Даны данные f,h1,h2,h3,h4 и изоморфизм e; явно сконструированное линейное эквивалентное отображение равно e.symm.

LaTeX

$$$(\mathrm{LinearEquiv.mk}\langle\langle f,h_1\rangle, h_2\rangle (\!\smash{e}) h_3 h_4 : M_2 \simeq_{\sigma'} M) = e^{-1}$$$

Lean4

@[simp]
theorem mk_coe' (f h₁ h₂ h₃ h₄) : (LinearEquiv.mk ⟨⟨f, h₁⟩, h₂⟩ (⇑e) h₃ h₄ : M₂ ≃ₛₗ[σ'] M) = e.symm :=
  symm_bijective.injective <| ext fun _ ↦ rfl

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