Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 20:59 27b0a763

View on Github →

feat(ring_theory/adjoin): adjoin_range_eq_range_aeval (#9179)

Estimated changes

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_range_eq_range_aeval

deleted theorem algebra.adjoin_singleton_eq_range

added theorem algebra.adjoin_singleton_eq_range_aeval

Modified src/ring_theory/adjoin/power_basis.lean

Modified src/ring_theory/adjoin_root.lean

Modified src/ring_theory/integral_closure.lean