Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 12:00 d6b4cd7b

View on Github →

chore(ring_theory/adjoin/basic): split (#9257) I want to use basic facts about adjoin in polynomial.basic.

Estimated changes

deleted theorem algebra.adjoin_eq_range
deleted theorem algebra.fg_trans
deleted theorem is_noetherian_ring_of_fg
deleted def subalgebra.fg
deleted theorem subalgebra.fg_bot
deleted theorem subalgebra.fg_def
deleted theorem subalgebra.fg_map
deleted theorem subalgebra.fg_of_fg_map
deleted theorem subalgebra.fg_prod
deleted theorem subalgebra.fg_top
added theorem algebra.fg_trans
added def subalgebra.fg
added theorem subalgebra.fg_bot
added theorem subalgebra.fg_def
added theorem subalgebra.fg_map
added theorem subalgebra.fg_prod
added theorem subalgebra.fg_top