aux_inj_roots_of_min_poly — Mathlib

English

Same injectivity result for the roots-of-minpoly construction: the function rootsOfMinPolyPiType F E K is injective.

Русский

Повторное утверждение инъективности для отображения корней минимального полинома: rootsOfMinPolyPiType F E K инъективно.

LaTeX

$$Injective (minpoly.rootsOfMinPolyPiType F E K)$$

Lean4

theorem aux_inj_roots_of_min_poly : Injective (rootsOfMinPolyPiType F E K) :=
  by
  intro f g h
  suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢
  rw [funext_iff] at h
  exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he => Subtype.ext_iff.mp (h ⟨e, he⟩)

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