Commit 2022-07-21 13:52 62b5bb74

View on Github →

refactor(field_theory/*): Refactor normal to use is_algebraic (#15421) This PR refactors normal to use is_algebraic rather than is_integral, as suggested by a TODO comment. I think the motivation is that is_algebraic is the preferred language when discussing fields.

Estimated changes

Modified src/field_theory/fixed.lean

Modified src/field_theory/galois.lean

modified theorem is_galois.integral

Modified src/field_theory/normal.lean

added theorem normal.is_algebraic

modified theorem normal.is_integral