Commit 2023-03-11 15:48 566f6de6

View on Github →

feat: port Algebra.Algebra.Subalgebra.Tower (#2790)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

added theorem Algebra.lmul_algebraMap

added theorem IsScalarTower.adjoin_range_toAlgHom

added theorem Subalgebra.coe_restrictScalars

added theorem Subalgebra.mem_restrictScalars

added def Subalgebra.ofRestrictScalars

added def Subalgebra.restrictScalars

added theorem Subalgebra.restrictScalars_injective

added theorem Subalgebra.restrictScalars_toSubmodule

added theorem Subalgebra.restrictScalars_top