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