Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-06 11:32 98e8408a

View on Github →

feat(geometry/manifold/algebra): left_invariant_derivation (#8108) In this PR we prove that left-invariant derivations are a Lie algebra.

Estimated changes

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

added theorem left_invariant_derivation.coe_add

added theorem left_invariant_derivation.coe_derivation

added theorem left_invariant_derivation.coe_derivation_injective

added def left_invariant_derivation.coe_fn_add_monoid_hom

added theorem left_invariant_derivation.coe_injective

added theorem left_invariant_derivation.coe_neg

added theorem left_invariant_derivation.coe_smul

added theorem left_invariant_derivation.coe_sub

added theorem left_invariant_derivation.coe_to_linear_map

added theorem left_invariant_derivation.coe_zero

added theorem left_invariant_derivation.commutator_apply

added theorem left_invariant_derivation.commutator_coe_derivation

added theorem left_invariant_derivation.comp_L

added def left_invariant_derivation.eval_at

added theorem left_invariant_derivation.eval_at_apply

added theorem left_invariant_derivation.eval_at_coe

added theorem left_invariant_derivation.eval_at_mul

added theorem left_invariant_derivation.ext

added theorem left_invariant_derivation.left_invariant'

added theorem left_invariant_derivation.left_invariant

added theorem left_invariant_derivation.leibniz

added theorem left_invariant_derivation.lift_add

added theorem left_invariant_derivation.lift_smul

added theorem left_invariant_derivation.lift_zero

added theorem left_invariant_derivation.map_add

added theorem left_invariant_derivation.map_neg

added theorem left_invariant_derivation.map_smul

added theorem left_invariant_derivation.map_sub

added theorem left_invariant_derivation.map_zero

added theorem left_invariant_derivation.to_derivation_eq_coe

added theorem left_invariant_derivation.to_fun_eq_coe

added structure left_invariant_derivation

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

added theorem smooth_left_mul_one

added theorem smooth_right_mul_one

Modified src/geometry/manifold/derivation_bundle.lean

modified theorem apply_fdifferential

added theorem apply_hfdifferential

deleted def fdifferential_map

added def hfdifferential

Modified src/ring_theory/derivation.lean

added theorem derivation.congr_fun