mathlib
eaf5cf6b - chore(number_theory/number_field/embeddings): golf (#16804)

Commit
3 years ago
chore(number_theory/number_field/embeddings): golf (#16804) Also golfs `bUnion_roots_finite` in *data/polynomial/ring_division*.
Author
Parents
Loading