Algebra.norm_algebraMap_sub_eq_eval_minpoly_pow
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_eval_minpoly_pow
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
instIsScalarTowerSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Divisor.instDistribMulActionAlgEquiv
instSMulAlgEquiv
instIsPrincipalIdealRingSubtypeMemValuationSubringToValuationSubring
instIsDiscreteValuationRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Pic0.instDistribMulActionAlgEquiv
instAlgebraSubtypeMemValuationSubringToValuationSubring
instMulActionAlgEquiv
AlgebraicCurve.Pic0.instSMulAlgEquiv
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom AlgebraicCurve.Place.mk.injEq
AlgebraicCurve.Divisor.degree_single AlgebraicCurve.Divisor.smul_single
AlgebraicCurve.Place.smul_toValuationSubring AlgebraicCurve.Place.heightOneSpectrum_asIdeal
AlgebraicCurve.Place.coe_algebraMap AlgebraicCurve.Place.ord_one
AlgebraicCurve.Place.coe_smulRingEquiv_apply AlgebraicCurve.Pic0.coe_degZeroSMulHom
AlgebraicCurve.Place.deg_smul AlgebraicCurve.Pic0.mk_zero AlgebraicCurve.Place.mk.sizeOf_spec
AlgebraicCurve.Divisor.degree_smul AlgebraicCurve.Pic0.mk_add AlgebraicCurve.Place.ord_zero
AlgebraicCurve.Place.ofHeightOneSpectrum_toValuationSubring
open PolynomialLean source · statement
theorem _root_.Algebra.norm_algebraMap_sub_eq_eval_minpoly_pow
{K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) (c : K) :
Algebra.norm K (algebraMap K L c - x)
= ((minpoly K x).eval c) ^ (Module.finrank K L / (minpoly K x).natDegree)