Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-17 15:27 97fc8ce1

View on Github →

refactor(algebra/lie/basic): unbundle the action in lie_module (#4959)

Estimated changes

Modified src/algebra/lie/basic.lean

modified theorem add_lie

modified theorem commutative_ring_iff_abelian_lie_ring

modified theorem gsmul_lie

added theorem leibniz_lie

deleted theorem lie_act

modified theorem lie_add

modified def lie_algebra.ad

added theorem lie_algebra.ad_apply

deleted theorem lie_algebra.endo_algebra_bracket

modified def lie_algebra.of_associative_algebra_hom

modified theorem lie_algebra.of_associative_algebra_hom_apply

modified theorem lie_algebra.of_associative_algebra_hom_comp

modified theorem lie_algebra.of_associative_algebra_hom_id

modified theorem lie_gsmul

added theorem lie_jacobi

added theorem lie_lie

modified theorem lie_mem_left

deleted def lie_module.of_endo_morphism

added def lie_module.to_endo_morphism

modified theorem lie_neg

modified theorem lie_ring.of_associative_ring_bracket

modified theorem lie_self

modified theorem lie_skew

modified theorem lie_smul

added def lie_submodule.quotient.action_as_endo_map

added def lie_submodule.quotient.action_as_endo_map_bracket

deleted theorem lie_submodule.quotient.lie_quotient_action_apply

modified structure lie_submodule

modified theorem lie_zero

modified theorem neg_lie

modified theorem smul_lie

modified theorem zero_lie

Modified src/algebra/lie/classical.lean

modified theorem lie_algebra.special_linear.sl_non_abelian

Modified src/linear_algebra/basic.lean

added theorem linear_map.mul_eq_comp

Deleted src/linear_algebra/linear_action.lean

deleted def linear_action.of_endo_map

deleted def linear_action.to_endo_map

deleted theorem linear_action_act_add

deleted theorem linear_action_act_smul

deleted theorem linear_action_add_act

deleted theorem linear_action_smul_act

deleted theorem linear_action_zero

deleted theorem zero_linear_action

Modified src/ring_theory/derivation.lean

modified theorem derivation.commutator_coe_linear_map

added theorem derivation.sub_apply

Modified test/transport/basic.lean

deleted def lie_ring.map