Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-27 01:10 825edd3c

View on Github →

chore(ring_theory): protect algebra.is_integral (#18178)

Estimated changes

Modified src/field_theory/intermediate_field.lean

Modified src/field_theory/minpoly/is_integrally_closed.lean

modified def algebra.adjoin.power_basis'

Modified src/ring_theory/adjoin/power_basis.lean

Modified src/ring_theory/discriminant.lean

Modified src/ring_theory/integral_closure.lean

deleted def algebra.is_integral

modified theorem algebra.is_integral_trans

modified theorem is_integral_of_surjective

modified theorem is_integral_quotient_of_is_integral

modified theorem is_integral_trans

Modified src/ring_theory/norm.lean

Modified src/ring_theory/trace.lean

modified theorem algebra.is_integral_trace