Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 07:29 cceedbca

View on Github →

feat(ring_theory/derivation): The Kähler differential module is functorial (#17018)

Estimated changes

Modified src/ring_theory/derivation.lean

added def derivation.comp_algebra_map

added def derivation.restrict_scalars

added def kaehler_differential.from_ideal

added def kaehler_differential.map

added theorem kaehler_differential.map_D

added def kaehler_differential.map_base_change

added theorem kaehler_differential.map_base_change_tmul

added theorem kaehler_differential.map_comp_der

added theorem kaehler_differential.map_surjective_of_surjective