Commit 2026-05-08 11:55 56972716

View on Github →

feat(RingTheory/Ideal/IsAugmentation): define the concept of an augmentation ideal (#37744) Define an augmentation ideal in an R-algebra A: this is an Ideal A which is a complement to ⊥ : Subalgebra R A in A. (This subalgebra consists of R-multiples of 1.) Co-authored with: @mariainesdff

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

added theorem Subalgebra.codisjoint_one_iff

added theorem Subalgebra.disjoint_one_iff

modified theorem Subalgebra.range_isScalarTower_toAlgHom

added theorem Subalgebra.restrictScalars_one

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

added theorem Submodule.codisjoint_restrictScalars_iff

added theorem Submodule.disjoint_restrictScalars_iff

added theorem Submodule.isCompl_restrictScalars_iff

added theorem Submodule.restrictScalars_restrictScalars

Created Mathlib/RingTheory/Ideal/IsAugmentation.lean

added def Ideal.IsAugmentation

added theorem Ideal.isAugmentation_iff

added theorem Ideal.isAugmentation_subalgebra_iff