Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-06 10:46 28e5032b

View on Github →

feat(ring_theory/derivation): Endomorphisms of the Kähler differential module (#15854)

Estimated changes

Modified src/algebra/module/submodule/basic.lean

Modified src/group_theory/group_action/sub_mul_action.lean

Modified src/ring_theory/derivation.lean

added def kaehler_differential.End_equiv

added theorem kaehler_differential.End_equiv_aux

added def kaehler_differential.End_equiv_aux_equiv

added def kaehler_differential.End_equiv_derivation'

added def kaehler_differential.quotient_cotangent_ideal

added def kaehler_differential.quotient_cotangent_ideal_ring_equiv

added def linear_equiv.comp_der

Modified src/ring_theory/ideal/cotangent.lean

added def ideal.quot_cotangent

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.map_eq_submodule_map

Modified src/ring_theory/ideal/quotient.lean