conj_id — Mathlib

English

If M2 and M3 are linearly isomorphic, then the spaces of linear maps from M into M2 and from M into M3 are linearly isomorphic via postcomposition with the given isomorphism.

Русский

Если M2 и M3 линейно изоморфны, то пространства линейных отображений из M в M2 и из M в M3 изоморфны линейно по посткомпозиции с данным изоморфизмом.

LaTeX

$$$ (M \to_{\mathbb{R}} M_2) \simeq_{\ell} (M \to_{\mathbb{R}} M_3) $$$

Lean4

@[simp]
theorem conj_id (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') : e.conj LinearMap.id = LinearMap.id := by simp [conj_apply]

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