Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-01 19:12 b608348f

View on Github →

chore(ring_theory/derivation): split file (#19138) The Stone-Weierstrass theorem shouldn't require the definition of Lie algebras.

Estimated changes

Modified src/data/mv_polynomial/derivation.lean

Modified src/geometry/manifold/algebra/left_invariant_derivation.lean

Modified src/geometry/manifold/derivation_bundle.lean

Renamed src/ring_theory/derivation.lean to src/ring_theory/derivation/basic.lean

deleted theorem derivation.commutator_apply

deleted theorem derivation.commutator_coe_linear_map

deleted def derivation_to_square_zero_equiv_lift

deleted def derivation_to_square_zero_of_lift

deleted theorem derivation_to_square_zero_of_lift_apply

deleted def diff_to_ideal_of_quotient_comp_eq

deleted theorem diff_to_ideal_of_quotient_comp_eq_apply

deleted def lift_of_derivation_to_square_zero

deleted theorem lift_of_derivation_to_square_zero_mk_apply

Created src/ring_theory/derivation/lie.lean

added theorem derivation.commutator_apply

added theorem derivation.commutator_coe_linear_map

Created src/ring_theory/derivation/to_square_zero.lean

added def derivation_to_square_zero_equiv_lift

added def derivation_to_square_zero_of_lift

added theorem derivation_to_square_zero_of_lift_apply

added def diff_to_ideal_of_quotient_comp_eq

added theorem diff_to_ideal_of_quotient_comp_eq_apply

added def lift_of_derivation_to_square_zero

added theorem lift_of_derivation_to_square_zero_mk_apply

Modified src/ring_theory/kaehler.lean