of_linearEquiv — Mathlib

English

If M and N are linearly isomorphic, then postcomposing the presentation with the isomorphism yields a presentation on N.

Русский

Если M и N линейно изоморфны, то посткомпоновка презентации с этим изоморфизмом образует презентацию на N.

LaTeX

$$$$ (solution.postcomp e.toLinearMap).IsPresentation $$$$

Lean4

theorem of_linearEquiv (e : M ≃ₗ[A] N) : (solution.postcomp e.toLinearMap).IsPresentation where
  bijective :=
    by
    have : (solution.postcomp e.toLinearMap).fromQuotient = e.toLinearMap.comp (solution.fromQuotient) := by aesop
    rw [this, LinearMap.coe_comp, LinearEquiv.coe_coe]
    exact Function.Bijective.comp e.bijective h.bijective

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