mathlib
d0323804 - feat(field_theory/normal): normal_of_alg_equiv (#5225)

Commit

5 years ago

feat(field_theory/normal): normal_of_alg_equiv (#5225) Proves that normal is preserved by an alg_equiv

Author

tb65536

Parents