Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 20:46 40214fcb

View on Github →

feat(ring_theory/derivations): stab on derivations (#3688)

Estimated changes

Modified src/algebra/classical_lie_algebras.lean

Modified src/algebra/group/basic.lean

added theorem eq_one_of_left_cancel_mul_self

added theorem eq_one_of_mul_self_left_cancel

added theorem eq_one_of_mul_self_right_cancel

added theorem eq_one_of_right_cancel_mul_self

Modified src/algebra/group/defs.lean

Modified src/algebra/lie_algebra.lean

deleted def lie_algebra.of_associative_algebra

deleted def lie_ring.of_associative_ring

deleted def matrix.lie_algebra

deleted def matrix.lie_ring

deleted theorem ring_commutator.add_left

deleted theorem ring_commutator.add_right

deleted theorem ring_commutator.alternate

added theorem ring_commutator.commutator

deleted def ring_commutator.commutator

deleted theorem ring_commutator.jacobi

Modified src/algebra/module/basic.lean

modified theorem is_linear_map.is_linear_map_smul

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/hahn_banach.lean

Modified src/analysis/normed_space/operator_norm.lean

modified def continuous_linear_map.smul_algebra_right

Modified src/data/complex/module.lean

Modified src/data/monoid_algebra.lean

Modified src/group_theory/group_action.lean

modified theorem smul_assoc

Modified src/representation_theory/maschke.lean

Modified src/ring_theory/algebra.lean

added theorem algebra_compatible_smul

modified def linear_map_algebra_module

added theorem map_smul_eq_smul_map

deleted def module.restrict_scalars'

deleted def module.restrict_scalars

deleted theorem module.restrict_scalars_smul_def

added def semimodule.restrict_scalars'

added def semimodule.restrict_scalars

added theorem semimodule.restrict_scalars_smul_def

modified def smul_algebra_right

deleted theorem smul_algebra_smul

modified theorem smul_algebra_smul_comm

modified def subspace.restrict_scalars

Created src/ring_theory/derivation.lean

added theorem derivation.Rsmul_apply

added theorem derivation.add_apply

added theorem derivation.coe_fn_coe

added theorem derivation.coe_injective

added def derivation.commutator

added theorem derivation.commutator_apply

added theorem derivation.commutator_coe_linear_map

added theorem derivation.ext

added theorem derivation.leibniz

added theorem derivation.map_add

added theorem derivation.map_algebra_map

added theorem derivation.map_neg

added theorem derivation.map_one_eq_zero

added theorem derivation.map_smul

added theorem derivation.map_sub

added theorem derivation.map_zero

added theorem derivation.smul_apply

added theorem derivation.smul_to_linear_map_coe

added theorem derivation.to_fun_eq_coe

added structure derivation

added def linear_map.comp_der

added theorem linear_map.comp_der_apply