Commit 2023-06-02 11:07 c0a6eca9

View on Github →

feat: port RingTheory.Derivation.Basic (#4575)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Derivation/Basic.lean

added theorem Derivation.add_apply

added def Derivation.coeFnAddMonoidHom

added theorem Derivation.coeFn_coe

added theorem Derivation.coe_add

added theorem Derivation.coe_add_linearMap

added theorem Derivation.coe_comp

added theorem Derivation.coe_injective

added theorem Derivation.coe_mk'

added theorem Derivation.coe_mk'_linearMap

added theorem Derivation.coe_neg

added theorem Derivation.coe_neg_linearMap

added theorem Derivation.coe_smul

added theorem Derivation.coe_smul_linearMap

added theorem Derivation.coe_sub

added theorem Derivation.coe_sub_linearMap

added theorem Derivation.coe_to_linearMap_comp

added theorem Derivation.coe_zero

added theorem Derivation.coe_zero_linearMap

added theorem Derivation.congr_fun

added theorem Derivation.eqOn_adjoin

added theorem Derivation.ext

added theorem Derivation.ext_of_adjoin_eq_top

added theorem Derivation.leibniz

added theorem Derivation.leibniz_inv

added theorem Derivation.leibniz_invOf

added theorem Derivation.leibniz_of_mul_eq_one

added theorem Derivation.leibniz_pow

added def Derivation.llcomp

added theorem Derivation.map_algebraMap

added theorem Derivation.map_coe_int

added theorem Derivation.map_coe_nat

added theorem Derivation.map_one_eq_zero

added theorem Derivation.map_smul

added theorem Derivation.map_smul_of_tower

added theorem Derivation.map_sum

added def Derivation.mk'

added theorem Derivation.mk_coe

added theorem Derivation.neg_apply

added theorem Derivation.smul_apply

added theorem Derivation.sub_apply

added theorem Derivation.toFun_eq_coe

added theorem Derivation.zero_apply

added structure Derivation

added def LinearEquiv.compDer

added def LinearMap.compDer