Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 10:36 03062ea4

View on Github →

feat(ring_theory/integral_closure): The product of the leading coeff and the root is integral. (#10807)

Estimated changes

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_leading_coeff_smul

added theorem leading_coeff_smul_normalize_scale_roots

added def normalize_scale_roots

added theorem normalize_scale_roots_coeff_mul_leading_coeff_pow

added theorem normalize_scale_roots_degree

added theorem normalize_scale_roots_eval₂_leading_coeff_mul

added theorem normalize_scale_roots_monic

added theorem normalize_scale_roots_support

added theorem ring_hom.is_integral_elem_leading_coeff_mul