Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-10 12:28
913dc471
View on Github →
feat(RingTheory/Presentation): Develop API for presentations of algebras. (
#12518
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/RingTheory/Generators.lean
added
theorem
Algebra.Generators.Cotangent.ext
added
def
Algebra.Generators.Cotangent.map
added
theorem
Algebra.Generators.Cotangent.map_mk
added
def
Algebra.Generators.Cotangent.mk
added
theorem
Algebra.Generators.Cotangent.mk_surjective
added
def
Algebra.Generators.Cotangent.of
added
theorem
Algebra.Generators.Cotangent.of_add
added
theorem
Algebra.Generators.Cotangent.of_val
added
theorem
Algebra.Generators.Cotangent.of_zero
added
theorem
Algebra.Generators.Cotangent.smul_eq_zero_of_mem
added
def
Algebra.Generators.Cotangent.val
added
theorem
Algebra.Generators.Cotangent.val_add
added
theorem
Algebra.Generators.Cotangent.val_mk
added
theorem
Algebra.Generators.Cotangent.val_of
added
theorem
Algebra.Generators.Cotangent.val_smul'''
added
theorem
Algebra.Generators.Cotangent.val_smul''
added
theorem
Algebra.Generators.Cotangent.val_smul'
added
theorem
Algebra.Generators.Cotangent.val_smul
added
theorem
Algebra.Generators.Cotangent.val_zero
added
def
Algebra.Generators.Cotangent
added
theorem
Algebra.Generators.Hom.algebraMap_toAlgHom
added
theorem
Algebra.Generators.Hom.comp_id
added
def
Algebra.Generators.Hom.equivAlgHom
added
theorem
Algebra.Generators.Hom.id_comp
added
def
Algebra.Generators.Hom.toAlgHom
added
theorem
Algebra.Generators.Hom.toAlgHom_C
added
theorem
Algebra.Generators.Hom.toAlgHom_X
added
structure
Algebra.Generators.Hom
added
def
Algebra.Generators.Simps.σ
added
theorem
Algebra.Generators.aeval_val_σ
added
theorem
Algebra.Generators.algebraMap_apply
added
theorem
Algebra.Generators.algebraMap_eq
added
theorem
Algebra.Generators.algebraMap_surjective
added
def
Algebra.Generators.comp
added
def
Algebra.Generators.defaultHom
added
def
Algebra.Generators.extendScalars
added
def
Algebra.Generators.ofAlgHom
added
def
Algebra.Generators.ofComp
added
def
Algebra.Generators.ofSet
added
def
Algebra.Generators.ofSurjective
added
def
Algebra.Generators.self
added
def
Algebra.Generators.toComp
added
def
Algebra.Generators.toExtendScalars
added
def
Algebra.Generators.σ
added
theorem
Algebra.Generators.σ_injective
added
theorem
Algebra.Generators.σ_smul
added
structure
Algebra.Generators
Modified
Mathlib/RingTheory/Ideal/Cotangent.lean
added
def
Ideal.mapCotangent
added
theorem
Ideal.mapCotangent_toCotangent