Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-06 14:33 eaf5cf6b

View on Github →

chore(number_theory/number_field/embeddings): golf (#16804) Also golfs bUnion_roots_finite in data/polynomial/ring_division.

Estimated changes

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/is_alg_closed/basic.lean

added theorem algebra.is_algebraic.range_eval_eq_root_set_minpoly

Modified src/number_theory/number_field/embeddings.lean

modified theorem number_field.embeddings.coeff_bdd_of_norm_le

deleted theorem number_field.embeddings.range_eq_roots

added theorem number_field.embeddings.range_eval_eq_root_set_minpoly

deleted theorem number_field.embeddings.rat_range_eq_roots