English
The map rootsOfMinPolyPiType(F,E,K) that associates to each F-algebra homomorphism the tuple of roots of the corresponding minimal polynomials on a finite basis is injective; i.e., the roots determine the homomorphism uniquely.
Русский
Отображение, сопоставляющее каждому F-алгему гомоморфизм на соответствующий набор корней минимальных полиномов по основанию, инъективно; корни однозначно определяют гомоморфизм.
LaTeX
$$Injective (minpoly.rootsOfMinPolyPiType F E K)$$
Lean4
/-- Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x -/
def rootsOfMinPolyPiType (φ : E →ₐ[F] K) (x : range (Module.finBasis F E : _ → E)) :
{ l : K // l ∈ (minpoly F x.1).aroots K } :=
⟨φ x, by
rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val), ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]⟩
