Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 14:53 753ef903

View on Github →

feat(ring_theory/derivation): Construction of the module of Kähler differentials. (#16047)

Estimated changes

Modified src/ring_theory/derivation.lean

added def derivation.lift_kaehler_differential

added theorem derivation.lift_kaehler_differential_D

added theorem derivation.lift_kaehler_differential_apply

added theorem derivation.lift_kaehler_differential_comp

added theorem derivation.lift_kaehler_differential_unique

deleted def derivation_module.ideal

deleted theorem derivation_module.one_smul_sub_smul_one_mem_ideal

deleted theorem derivation_module.span_range_eq_ideal

deleted theorem derivation_module.submodule_span_range_eq_ideal

added def kaehler_differential.D

added theorem kaehler_differential.D_apply

added def kaehler_differential.D_linear_map

added theorem kaehler_differential.D_linear_map_apply

added theorem kaehler_differential.D_tensor_product_to

added def kaehler_differential.ideal

added def kaehler_differential.linear_map_equiv_derivation

added theorem kaehler_differential.one_smul_sub_smul_one_mem_ideal

added theorem kaehler_differential.span_range_derivation

added theorem kaehler_differential.span_range_eq_ideal

added theorem kaehler_differential.submodule_span_range_eq_ideal

added theorem kaehler_differential.tensor_product_to_surjective

added def kaehler_differential