Commit 2023-03-17 16:27 fede9482

View on Github →

feat: port RingTheory.AlgebraTower (#2586) simps is generating a lemma that the simpNF linter is having an issue again. Guess manual replacement of this lemma is the way to go, bit too sleepy to do that now though. Feel free to jump in!

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/AlgebraTower.lean

added def AlgHom.extendScalars

added def AlgHom.restrictDomain

added theorem Basis.algebraMapCoeffs_apply

added theorem Basis.algebraMap_injective

added theorem Basis.coe_algebraMapCoeffs

added theorem Basis.smul_apply

added theorem Basis.smul_repr

added theorem Basis.smul_repr_mk

added def IsScalarTower.Invertible.algebraTower

added def IsScalarTower.invertibleAlgebraCoeNat

added def algHomEquivSigma

added theorem linearIndependent_smul