Commit 2023-04-02 14:13 445481f9

View on Github →

feat: port RingTheory.Adjoin.Tower (#3210)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/Tower.lean

added theorem Algebra.adjoin_algebraMap

added theorem Algebra.adjoin_res_eq_adjoin_res

added theorem Algebra.adjoin_restrictScalars

added theorem Algebra.fg_trans'

added theorem exists_subalgebra_of_fg

added theorem fg_of_fg_of_fg