Commit 2023-07-08 16:04 a3b66ecb

View on Github →

feat: port RingTheory.Kaehler (#4668)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Created Mathlib/RingTheory/Kaehler.lean

added def Derivation.compAlgebraMap

added def Derivation.liftKaehlerDifferential

added theorem Derivation.liftKaehlerDifferential_D

added theorem Derivation.liftKaehlerDifferential_apply

added theorem Derivation.liftKaehlerDifferential_comp

added theorem Derivation.liftKaehlerDifferential_comp_D

added theorem Derivation.liftKaehlerDifferential_unique

added def Derivation.tensorProductTo

added theorem Derivation.tensorProductTo_mul

added theorem Derivation.tensorProductTo_tmul

added def KaehlerDifferential.D

added def KaehlerDifferential.DLinearMap

added theorem KaehlerDifferential.DLinearMap_apply

added theorem KaehlerDifferential.D_apply

added theorem KaehlerDifferential.D_tensorProductTo

added theorem KaehlerDifferential.End_equiv_aux

added theorem KaehlerDifferential.derivationQuotKerTotal_apply

added theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_total

added def KaehlerDifferential.endEquivAuxEquiv

added def KaehlerDifferential.fromIdeal

added theorem KaehlerDifferential.kerTotal_eq

added theorem KaehlerDifferential.kerTotal_map

added theorem KaehlerDifferential.kerTotal_mkQ_single_add

added theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap

added theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one

added theorem KaehlerDifferential.kerTotal_mkQ_single_mul

added theorem KaehlerDifferential.kerTotal_mkQ_single_smul

added def KaehlerDifferential.linearMapEquivDerivation

added def KaehlerDifferential.map

added theorem KaehlerDifferential.mapBaseChange_tmul

added theorem KaehlerDifferential.map_D

added theorem KaehlerDifferential.map_compDer

added theorem KaehlerDifferential.map_surjective_of_surjective

added theorem KaehlerDifferential.one_smul_sub_smul_one_mem_ideal

added theorem KaehlerDifferential.quotKerTotalEquiv_symm_comp_D

added def KaehlerDifferential.quotientCotangentIdeal

added def KaehlerDifferential.quotientCotangentIdealRingEquiv

added theorem KaehlerDifferential.span_range_derivation

added theorem KaehlerDifferential.span_range_eq_ideal

added theorem KaehlerDifferential.submodule_span_range_eq_ideal

added theorem KaehlerDifferential.tensorProductTo_surjective

added theorem KaehlerDifferential.total_surjective

added def KaehlerDifferential