Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-19 12:44 4113db58

View on Github →

feat(ring_theory): the trace of an integral element is integral (#8702) This PR uses trace_gen_eq_sum_roots and trace_trace to show the trace of an integral element x : L over K is a multiple of the sum of all conjugates of x, and concludes that the trace of x is integral.

Estimated changes

Modified src/data/polynomial/eval.lean

added theorem polynomial.eval₂_dvd

added theorem polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero

Modified src/field_theory/minpoly.lean

added theorem minpoly.aeval_of_is_scalar_tower

Modified src/ring_theory/integral_closure.lean

added theorem is_integral.gsmul

added theorem is_integral.multiset_prod

added theorem is_integral.multiset_sum

added theorem is_integral.nsmul

added theorem is_integral.pow

added theorem is_integral.prod

added theorem is_integral.sum

Modified src/ring_theory/trace.lean

added theorem algebra.is_integral_trace

deleted theorem algebra.trace_gen_eq_sum_roots

added theorem intermediate_field.adjoin_simple.trace_gen_eq_sum_roots

added theorem intermediate_field.adjoin_simple.trace_gen_eq_zero

added theorem power_basis.trace_gen_eq_sum_roots

added theorem trace_eq_sum_roots