LieDeriv.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

53 declarations, 0 contain sorry, 0 declared as axioms

Lie derivatives of smooth functions on `GL n ℝ`

The C^∞ functions on GL n ℝ and the action on them of 𝔤𝔩 n ℝ and of its complexification 𝔤𝔩 n ℂ by left invariant differential operators. This is the analytic machinery behind condition (c) in the Borel-Jacquet definition of an automorphic form; see FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet for that definition, and Borel and Jacquet's Corvallis article, the reference below, for its source.

Main declarations

All in the namespace Matrix.GeneralLinearGroup unless qualified otherwise:

AutomorphicForm.LieDerivAux.fderiv_rightDeriv_apply and …_sub_comm: the product rule and bracket identity for the operator F ↦ fun M => fderiv ℝ F M (M * X) over an abstract normed algebra.
IsSmoothOnGL and smoothGL: the C^∞ functions on GL n ℝ, as a predicate and as a ℂ-submodule.
expGL and lieDerivFun: the matrix exponential as an element of GL n ℝ, and the left invariant derivative (X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}.
lieDeriv and lieDerivC: the actions on smoothGL n of 𝔤𝔩 n ℝ and of its complexification 𝔤𝔩 n ℂ, with their bracket identities lieDeriv_bracket and lieDerivC_bracket.

Implementation notes

Smoothness on GL n ℝ is phrased as the existence of a C^∞ extension to the open set of invertible matrices (IsSmoothOnGL), rather than through a manifold structure: the normed ring instances on Matrix n n ℝ that would give GL n ℝ a chart are scoped, and conflict with the product topology that GL n ℝ already carries.

X ∈ 𝔤𝔩 n ℝ acts by differentiating along the one-parameter subgroup, (X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}; this equals fderiv ℝ F y (y * X) for any C^∞ extension F of φ (lieDerivFun_eq_fderiv), through which every algebraic property is proved. The bracket identity is the product rule plus symmetry of the second derivative.

The product rule is proved over an abstract finite-dimensional normed ℝ-algebra and instantiated at Matrix n n ℝ. That is forced: Mathlib's norms on Matrix n n ℝ are scoped instances while its topology is global, so instance search cannot assemble SeminormedAddCommGroup (Matrix n n ℝ →L[ℝ] ℂ) for the written-out type even though the instance term typechecks, and the second-derivative lemmas behind the product rule need that instance as an argument. Instantiating an abstract lemma supplies its instance arguments instead of searching for them.

References:

A. Borel and H. Jacquet, Automorphic forms and automorphic representations, in Automorphic Forms, Representations and L-functions (Corvallis), Proc. Sympos. Pure Math. 33, Part 1, Amer. Math. Soc. (1979), 189–207; §4.

Imports (9)

Imported by 3 files

def AutomorphicForm.LieDerivAux.mulRightL Right multiplication by X, as a continuous linear map line 98 source
Source documentation
Right multiplication by X, as a continuous linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedRing, NormedAlgebra, Real, FiniteDimensional, ContinuousLinearMap, RingHom.id
Proof uses: LinearEquiv, LinearMap, LinearMap.toContinuousLinearMap, LinearMap.mulRight
59 instances, coercions and auxiliary constants left out.
```
noncomputable def mulRightL (X : A) : A →L[ℝ] A :=
…
```
lemma AutomorphicForm.LieDerivAux.mulRightL_apply line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedRing, NormedAlgebra, Real, FiniteDimensional, Eq, ContinuousLinearMap, RingHom.id, AutomorphicForm.LieDerivAux.mulRightL, HMul.hMul
Proof uses: of_eq_true, eq_self
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma AutomorphicForm.LieDerivAux.fderiv_rightDeriv_apply Documented declaration: fderiv_rightDeriv_apply line 107 source
Source documentation
The product rule for the left invariant derivative F ↦ fun M => D F M (M * X): its derivative at y in the direction v picks up the first-order term D F y (v * X), from differentiating M ↦ M * X, and the second-order term D² F y v (y * X).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedRing, NormedAlgebra, Real, FiniteDimensional, Complex, ContDiffAt, ENat, Top.top, Eq, ContinuousLinearMap, RingHom.id, fderiv, HMul.hMul, HAdd.hAdd
Proof uses: HasFDerivAt, DifferentiableAt.hasFDerivAt, ContDiffAt.differentiableAt, ContDiffAt.fderiv_right, of_eq_true, LE.le, WithTop, Not, OfNat.ofNat, Eq.trans, False, True, congrArg, not_false_eq_true, AutomorphicForm.LieDerivAux.mulRightL, ContinuousLinearMap.hasFDerivAt, Function.comp, Prod, Prod.fst, Prod.snd and 14 more
199 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma fderiv_rightDeriv_apply {F : A → ℂ} {y : A} (hF : ContDiffAt ℝ ∞ F y) (X v : A) :
    fderiv ℝ (fun M => fderiv ℝ F M (M * X)) y v
      = fderiv ℝ F y (v * X) + fderiv ℝ (fderiv ℝ F) y v (y * X) := by
…
```
lemma AutomorphicForm.LieDerivAux.fderiv_rightDeriv_sub_comm The commutator of two left invariant derivatives is the left invariant derivative along the commutator: the second-order terms cancel by symmetry of the second derivative line 121 source
Source documentation
The commutator of two left invariant derivatives is the left invariant derivative along the commutator: the second-order terms cancel by symmetry of the second derivative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedRing, NormedAlgebra, Real, FiniteDimensional, Complex, ContDiffAt, ENat, Top.top, Eq, HSub.hSub, ContinuousLinearMap, RingHom.id, fderiv, HMul.hMul
Proof uses: LE.le, WithTop, minSmoothness, OfNat.ofNat, Nat, Eq.mpr, id, congrArg, minSmoothness_of_isRCLikeNormedField, Iff.mpr, WithTop.coe_le_coe, le_top, IsSymmSndFDerivAt.eq, ContDiffAt.isSymmSndFDerivAt, HAdd.hAdd, AutomorphicForm.LieDerivAux.fderiv_rightDeriv_apply, of_eq_true, Eq.trans, Neg.neg, True and 47 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma fderiv_rightDeriv_sub_comm {F : A → ℂ} {y : A} (hF : ContDiffAt ℝ ∞ F y) (X Y : A) :
    fderiv ℝ (fun M => fderiv ℝ F M (M * Y)) y (y * X)
      - fderiv ℝ (fun M => fderiv ℝ F M (M * X)) y (y * Y)
      = fderiv ℝ F y (y * (X * Y - Y * X)) := by
…
```
def Matrix.GeneralLinearGroup.IsSmoothOnGL φ : GL n ℝ → ℂ is C^∞: it extends to a C^∞ function on the open set of invertible matrices line 146 source
Source documentation
φ : GL n ℝ → ℂ is C^∞: it extends to a C^∞ function on the open set of invertible matrices. Stating it this way avoids putting a manifold structure on GL n ℝ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex
Proof uses: Exists, Matrix, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq
17 instances, coercions and auxiliary constants left out.
```
def IsSmoothOnGL (φ : GL n ℝ → ℂ) : Prop :=
…
```
lemma Matrix.GeneralLinearGroup.isSmoothOnGL_const line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix.GeneralLinearGroup, Real
Proof uses: Exists.intro, Matrix, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq, And.intro, contDiffOn_const, rfl
17 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.IsSmoothOnGL.add line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, HAdd.hAdd
Proof uses: Matrix, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq, Exists.intro, And.intro, ContDiffOn.add, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.IsSmoothOnGL.const_smul line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, HSMul.hSMul
Proof uses: Matrix, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq, Exists.intro, And.intro, ContDiffOn.const_smul, of_eq_true, HMul.hMul, Eq.trans, True, congrFun', congrArg, eq_self
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.isOpen_setOf_isUnit The invertible matrices are an open set: they are the nonvanishing locus of det line 165 source
Source documentation
The invertible matrices are an open set: they are the nonvanishing locus of det.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, IsOpen, Matrix, Real, Set.ofPred, IsUnit
Proof uses: Eq, Set, Set.preimage, Matrix.det, Ne, OfNat.ofNat, Set.ext, of_eq_true, Iff, Membership.mem, Not, Eq.trans, True, congrFun', congrArg, funext, iff_self, Eq.mpr, id, IsOpen.preimage and 3 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma isOpen_setOf_isUnit : IsOpen {M : Matrix n n ℝ | IsUnit M} := by
…
```
lemma Matrix.GeneralLinearGroup.isUnit_coe line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, IsUnit, Matrix
Proof uses: Exists.intro, Units, Eq, rfl
8 instances, coercions and auxiliary constants left out.
def Matrix.GeneralLinearGroup.extendGL A choice of C^∞ extension of φ to the invertible matrices, when one exists line 177 source
Source documentation
A choice of C^∞ extension of φ to the invertible matrices, when one exists. Only its germ at each invertible matrix matters, by fderiv_extendGL_eq.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix
Proof uses: dite, Matrix.GeneralLinearGroup.IsSmoothOnGL, Classical.propDecidable, Exists.choose, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq, Not, OfNat.ofNat
20 instances, coercions and auxiliary constants left out.
```
noncomputable def extendGL (φ : GL n ℝ → ℂ) : Matrix n n ℝ → ℂ :=
…
```
lemma Matrix.GeneralLinearGroup.contDiffOn_extendGL line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, ContDiffOn, Matrix, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Matrix.GeneralLinearGroup.extendGL, Set.ofPred, IsUnit
Proof uses: Eq.mpr, dite, Classical.propDecidable, Exists.choose, And, Eq, Not, OfNat.ofNat, id, congrArg, Matrix.GeneralLinearGroup.extendGL.eq_1, dif_pos, And.left, Exists.choose_spec
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.extendGL_coe line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Eq, Matrix.GeneralLinearGroup.extendGL, Matrix
Proof uses: Eq.mpr, dite, Classical.propDecidable, Exists.choose, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Not, OfNat.ofNat, id, congrArg, Matrix.GeneralLinearGroup.extendGL.eq_1, dif_pos, And.right, Exists.choose_spec
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.contDiffAt_extendGL line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, ContDiffAt, Matrix, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Matrix.GeneralLinearGroup.extendGL
Proof uses: ContDiffOn.contDiffAt, Set.ofPred, IsUnit, Matrix.GeneralLinearGroup.contDiffOn_extendGL, IsOpen.mem_nhds, Matrix.GeneralLinearGroup.isOpen_setOf_isUnit, Matrix.GeneralLinearGroup.isUnit_coe
36 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.fderiv_extendGL_eq The derivative of the chosen extension at an invertible matrix does not depend on the choice: any two extensions of φ agree on the open set of invertible matrices line 198 source
Source documentation
The derivative of the chosen extension at an invertible matrix does not depend on the choice: any two extensions of φ agree on the open set of invertible matrices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix, Matrix.GeneralLinearGroup.IsSmoothOnGL, Eq, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL
Proof uses: Filter.EventuallyEq.fderiv_eq, Filter.mp_mem, nhds, Set.ofPred, IsUnit, IsOpen.mem_nhds, Matrix.GeneralLinearGroup.isOpen_setOf_isUnit, Matrix.GeneralLinearGroup.isUnit_coe, Filter.univ_mem', Membership.mem, Set, id, Units, Eq.mpr, congrArg, Matrix.GeneralLinearGroup.extendGL_coe, Eq.refl
73 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma fderiv_extendGL_eq {φ : GL n ℝ → ℂ} {F : Matrix n n ℝ → ℂ} (hφ : IsSmoothOnGL φ)
    (hF : ∀ y : GL n ℝ, F (y : Matrix n n ℝ) = φ y) (y : GL n ℝ) :
    fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) = fderiv ℝ F (y : Matrix n n ℝ) := by
…
```
Mentions: Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix.GeneralLinearGroup.extendGL
def Matrix.GeneralLinearGroup.expGL The exponential of a matrix, as an element of GL n ℝ: exp X is invertible with inverse exp (-X) line 216 source
Source documentation
The exponential of a matrix, as an element of GL n ℝ: exp X is invertible with inverse exp (-X).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Matrix.GeneralLinearGroup
Proof uses: IsUnit.unit, Matrix.frobeniusNormedRing, NormedSpace.exp
11 instances, coercions and auxiliary constants left out.
```
noncomputable def expGL (X : Matrix n n ℝ) : GL n ℝ := (NormedSpace.isUnit_exp X).unit
…
```
lemma Matrix.GeneralLinearGroup.coe_expGL line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Eq, Matrix.GeneralLinearGroup.expGL, NormedSpace.exp
Proof uses: IsUnit.unit_spec, Matrix.frobeniusNormedRing, NormedSpace.isUnit_exp, Matrix.frobeniusNormedAlgebra, Rat, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace
55 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.expGL_zero line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Eq, Matrix.GeneralLinearGroup, Real, Matrix.GeneralLinearGroup.expGL, OfNat.ofNat, Matrix
Proof uses: Units.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, NormedSpace.exp, Matrix.GeneralLinearGroup.coe_expGL, NormedSpace.exp_zero, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.lieDerivFun Documented declaration: lieDerivFun line 233 source
Source documentation
The left invariant derivative of φ along X: differentiate φ along the one-parameter subgroup t ↦ exp (t • X) acting on the right,
(X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}.
This is the derivative that condition (c) of the definition of an automorphic form is about: the left invariant vector field with value X at 1 has value y * X at y, and lieDerivFun_eq_fderiv identifies the two descriptions for C^∞ functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Matrix.GeneralLinearGroup, Complex
Proof uses: deriv, HMul.hMul, Matrix.GeneralLinearGroup.expGL, HSMul.hSMul, OfNat.ofNat
30 instances, coercions and auxiliary constants left out.
```
noncomputable def lieDerivFun (X : Matrix n n ℝ) (φ : GL n ℝ → ℂ) (y : GL n ℝ) : ℂ :=
…
```
lemma Matrix.GeneralLinearGroup.hasDerivAt_lieDerivFun Differentiating along the one-parameter subgroup computes the derivative of any smooth extension in the direction y * X line 238 source
Source documentation
Differentiating along the one-parameter subgroup computes the derivative of any smooth extension in the direction y * X.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, HasDerivAt, HMul.hMul, Matrix.GeneralLinearGroup.expGL, HSMul.hSMul, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, OfNat.ofNat
Proof uses: Matrix.frobeniusNormedRing, Matrix.frobeniusNormedAlgebra, NormedSpace.exp, HasDerivAt.const_mul, hasDerivAt_exp_smul_const, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, Eq, funext, Eq.mpr, id, congrArg, Eq.symm, Matrix.GeneralLinearGroup.extendGL_coe, of_eq_true, Eq.trans, True, congrFun', Matrix.GeneralLinearGroup.coe_expGL, eq_self and 25 more
183 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma hasDerivAt_lieDerivFun {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X : Matrix n n ℝ)
    (y : GL n ℝ) :
    HasDerivAt (fun t : ℝ => φ (y * expGL (t • X)))
      (fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) ((y : Matrix n n ℝ) * X)) 0 := by
…
```
Mentions: Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix.GeneralLinearGroup.expGL, Matrix.GeneralLinearGroup.extendGL
lemma Matrix.GeneralLinearGroup.lieDerivFun_eq_fderiv The one-parameter-subgroup description of the left invariant derivative agrees with the directional-derivative one line 258 source
Source documentation
The one-parameter-subgroup description of the left invariant derivative agrees with the directional-derivative one. Every algebraic property below is proved through this bridge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, HMul.hMul
Proof uses: HasDerivAt.deriv, Matrix.GeneralLinearGroup.expGL, HSMul.hSMul, OfNat.ofNat, Matrix.GeneralLinearGroup.hasDerivAt_lieDerivFun
89 instances, coercions and auxiliary constants left out.
```
lemma lieDerivFun_eq_fderiv {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X : Matrix n n ℝ)
    (y : GL n ℝ) :
    lieDerivFun X φ y
      = fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) ((y : Matrix n n ℝ) * X) :=
…
```
Mentions: Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix.GeneralLinearGroup.lieDerivFun, Matrix.GeneralLinearGroup.extendGL
lemma Matrix.GeneralLinearGroup.IsSmoothOnGL.lieDerivFun line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Matrix.GeneralLinearGroup.lieDerivFun
Proof uses: Exists.intro, And, ContDiffOn, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, ENat, Top.top, Set.ofPred, IsUnit, Eq, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, HMul.hMul, And.intro, Membership.mem, Set, ContDiffAt, ContDiffOn.contDiffAt and 17 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.smoothGL The ℂ-submodule of C^∞ functions on GL n ℝ, which is what the Lie algebra and hence the universal enveloping algebra acts on line 275 source
Source documentation
The ℂ-submodule of C^∞ functions on GL n ℝ, which is what the Lie algebra and hence the universal enveloping algebra acts on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Submodule, Complex, Matrix.GeneralLinearGroup, Real
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, Matrix.GeneralLinearGroup.IsSmoothOnGL, Membership.mem, Set, Matrix.GeneralLinearGroup.IsSmoothOnGL.add, Matrix.GeneralLinearGroup.IsSmoothOnGL.const_smul
18 instances, coercions and auxiliary constants left out.
```
def smoothGL (n : Type*) [Fintype n] [DecidableEq n] : Submodule ℂ (GL n ℝ → ℂ) where
…
```
lemma Matrix.GeneralLinearGroup.mem_smoothGL line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Iff, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.IsSmoothOnGL
Proof uses: Iff.rfl
16 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.lieDerivFun_add line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, HAdd.hAdd
Proof uses: funext, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, HasFDerivAt.fderiv, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, Matrix.frobeniusNormedRing, Matrix.frobeniusIsBoundedSMul, HasFDerivAt.add, DifferentiableAt.hasFDerivAt, ContDiffAt.differentiableAt, ENat, Top.top, Matrix.GeneralLinearGroup.contDiffAt_extendGL, of_eq_true, Not, WithTop, OfNat.ofNat and 16 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivFun_const_smul line 296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, HSMul.hSMul
Proof uses: funext, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, HasFDerivAt.fderiv, Matrix.frobeniusNormedAddCommGroup, Matrix.frobeniusNormedSpace, Matrix.frobeniusNormedRing, Matrix.frobeniusIsBoundedSMul, HasFDerivAt.const_smul, DifferentiableAt.hasFDerivAt, ContDiffAt.differentiableAt, ENat, Top.top, Matrix.GeneralLinearGroup.contDiffAt_extendGL, of_eq_true, Not, WithTop, OfNat.ofNat and 16 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivFun_zero_left line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Eq, Matrix.GeneralLinearGroup.lieDerivFun, OfNat.ofNat, Matrix
Proof uses: funext, of_eq_true, Eq.trans, True, congrFun', congrArg, deriv, HMul.hMul, Matrix.GeneralLinearGroup.expGL, HSMul.hSMul, smul_zero, Matrix.GeneralLinearGroup.expGL_zero, mul_one, congrFun, deriv_const', eq_self
62 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivFun_add_left line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, HAdd.hAdd
Proof uses: funext, of_eq_true, Eq.trans, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, HMul.hMul, True, congr, congrArg, Matrix.GeneralLinearGroup.lieDerivFun_eq_fderiv, mul_add, map_add, eq_self
58 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivFun_smul_left line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, HSMul.hSMul
Proof uses: funext, of_eq_true, Eq.trans, HMul.hMul, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, True, congr, congrArg, Matrix.GeneralLinearGroup.lieDerivFun_eq_fderiv, Algebra.mul_smul_comm, map_smul, eq_self
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivFun_const line 320 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Complex, Eq, Matrix.GeneralLinearGroup, Matrix.GeneralLinearGroup.lieDerivFun, OfNat.ofNat
Proof uses: funext, of_eq_true, Eq.trans, True, congrFun', congrArg, congrFun, deriv, deriv_const', eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.lieDeriv The left invariant derivative along X as a ℂ-linear endomorphism of the C^∞ functions on GL n ℝ line 327 source
Source documentation
The left invariant derivative along X as a ℂ-linear endomorphism of the C^∞ functions on GL n ℝ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL
Proof uses: LinearMap.mk, AddHom.mk, Subtype.mk, Matrix.GeneralLinearGroup.lieDerivFun
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def lieDeriv (X : Matrix n n ℝ) : smoothGL n →ₗ[ℂ] smoothGL n where
…
```
Mentions: Matrix.GeneralLinearGroup.smoothGL
lemma Matrix.GeneralLinearGroup.coe_lieDeriv line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Subtype, Matrix.GeneralLinearGroup, Complex, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Eq, LinearMap, RingHom.id, Matrix.GeneralLinearGroup.lieDeriv, Matrix.GeneralLinearGroup.lieDerivFun
Proof uses: rfl
28 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.lieDerivFun_bracket The commutator of two left invariant derivatives is the left invariant derivative along the commutator of the directions line 339 source
Source documentation
The commutator of two left invariant derivatives is the left invariant derivative along the commutator of the directions. This is the bracket identity that makes lieDeriv a Lie algebra homomorphism; the second-order terms cancel by symmetry of the second derivative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix, Eq, Matrix.GeneralLinearGroup.lieDerivFun, HSub.hSub, HMul.hMul
Proof uses: funext, ContinuousLinearMap, RingHom.id, fderiv, Matrix.GeneralLinearGroup.extendGL, Matrix.GeneralLinearGroup.fderiv_extendGL_eq, Matrix.GeneralLinearGroup.IsSmoothOnGL.lieDerivFun, Eq.symm, Matrix.GeneralLinearGroup.lieDerivFun_eq_fderiv, Eq.mpr, id, congrArg, Pi.sub_apply, Matrix.frobeniusNormedRing, Matrix.frobeniusNormedAlgebra, AutomorphicForm.LieDerivAux.fderiv_rightDeriv_sub_comm, Matrix.GeneralLinearGroup.contDiffAt_extendGL
75 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma lieDerivFun_bracket {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X Y : Matrix n n ℝ) :
    lieDerivFun (X * Y - Y * X) φ
      = lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ) := by
…
```
Mentions: Matrix.GeneralLinearGroup.IsSmoothOnGL, Matrix.GeneralLinearGroup.lieDerivFun
lemma Matrix.GeneralLinearGroup.lieDeriv_bracket line 355 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, HSub.hSub, HMul.hMul
Proof uses: LinearMap.ext, Subtype.ext, id, Matrix.GeneralLinearGroup.lieDerivFun_bracket, Subtype.property
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDeriv_zero line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, OfNat.ofNat, Matrix
Proof uses: LinearMap.ext, Subtype.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, Matrix.GeneralLinearGroup.lieDerivFun_zero_left, eq_self
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDeriv_add line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, HAdd.hAdd
Proof uses: LinearMap.ext, Subtype.ext, id, Matrix.GeneralLinearGroup.lieDerivFun_add_left, Subtype.property
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDeriv_real_smul line 367 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Real, Matrix, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, HSMul.hSMul
Proof uses: LinearMap.ext, Subtype.ext, id, Matrix.GeneralLinearGroup.lieDerivFun_smul_left, Subtype.property
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDeriv_neg line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, Neg.neg
Proof uses: Eq.mpr, HSMul.hSMul, OfNat.ofNat, id, congrArg, of_eq_true, Eq.trans, True, neg_smul, one_smul, eq_self, Matrix.GeneralLinearGroup.lieDeriv_real_smul, congrFun', Complex.ofReal_neg, Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval, Int, Mathlib.Tactic.Module.NF.cons, Prod.mk, HMul.hMul, RingHom and 43 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDeriv_sub line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Real, Eq, LinearMap, Complex, RingHom.id, Subtype, Matrix.GeneralLinearGroup, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDeriv, HSub.hSub
Proof uses: Eq.mpr, HAdd.hAdd, Neg.neg, id, congrArg, sub_eq_add_neg, Matrix.GeneralLinearGroup.lieDeriv_add, Matrix.GeneralLinearGroup.lieDeriv_neg
55 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.map_re_add line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Complex, Eq, Real, Matrix.map, HAdd.hAdd, Complex.re
Proof uses: Matrix.map_add, Complex.add_re
6 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.map_im_add line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Complex, Eq, Real, Matrix.map, HAdd.hAdd, Complex.im
Proof uses: Matrix.map_add, Complex.add_im
6 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.map_re_sub line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Complex, Eq, Real, Matrix.map, HSub.hSub, Complex.re
Proof uses: Matrix.map_sub, Complex.sub_re
6 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.map_im_sub line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Complex, Eq, Real, Matrix.map, HSub.hSub, Complex.im
Proof uses: Matrix.map_sub, Complex.sub_im
6 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.map_re_smul line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Matrix, Eq, Real, Matrix.map, HSMul.hSMul, Complex.re, HSub.hSub, Complex.im
Proof uses: Matrix.ext, of_eq_true, HMul.hMul, Eq.trans, True, congrFun', congrArg, Complex.mul_re, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.map_im_smul line 411 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Matrix, Eq, Real, Matrix.map, HSMul.hSMul, Complex.im, HAdd.hAdd, Complex.re
Proof uses: Matrix.ext, of_eq_true, HMul.hMul, Eq.trans, True, congrFun', congrArg, Complex.mul_im, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.map_re_mul line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Complex, Eq, Real, Matrix.map, HMul.hMul, Complex.re, HSub.hSub, Complex.im
Proof uses: Matrix.ext, of_eq_true, Finset.sum, Finset.univ, Eq.trans, True, congrFun', congrArg, Complex.re_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Complex.mul_re, Finset.sum_sub_distrib, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.map_im_mul line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Complex, Eq, Real, Matrix.map, HMul.hMul, Complex.im, HAdd.hAdd, Complex.re
Proof uses: Matrix.ext, of_eq_true, Finset.sum, Finset.univ, Eq.trans, True, congrFun', congrArg, Complex.im_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Complex.mul_im, Finset.sum_add_distrib, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.map_re_bracket The real part of a complex commutator, arranged as a difference of two real commutators line 433 source
Source documentation
The real part of a complex commutator, arranged as a difference of two real commutators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Complex, Eq, Real, Matrix.map, HSub.hSub, HMul.hMul, Complex.re, Complex.im
Proof uses: Eq.mpr, id, congrArg, Matrix.GeneralLinearGroup.map_re_sub, Matrix.GeneralLinearGroup.map_re_mul
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma map_re_bracket (Z W : Matrix n n ℂ) :
    (Z * W - W * Z).map Complex.re
      = (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re)
        - (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) := by
…
```
lemma Matrix.GeneralLinearGroup.map_im_bracket The imaginary part of a complex commutator, arranged as a sum of two real commutators line 441 source
Source documentation
The imaginary part of a complex commutator, arranged as a sum of two real commutators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Complex, Eq, Real, Matrix.map, HSub.hSub, HMul.hMul, Complex.im, HAdd.hAdd, Complex.re
Proof uses: Eq.mpr, id, congrArg, Matrix.GeneralLinearGroup.map_im_sub, Matrix.GeneralLinearGroup.map_im_mul
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma map_im_bracket (Z W : Matrix n n ℂ) :
    (Z * W - W * Z).map Complex.im
      = (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re)
        + (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im) := by
…
```
def Matrix.GeneralLinearGroup.lieDerivC The action of the complexified Lie algebra 𝔤𝔩 n ℂ of GL n ℝ on the C^∞ functions: X + i Y acts as lieDeriv X + i • lieDeriv Y line 452 source
Source documentation
The action of the complexified Lie algebra 𝔤𝔩 n ℂ of GL n ℝ on the C^∞ functions: X + i Y acts as lieDeriv X + i • lieDeriv Y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Complex, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL
Proof uses: HAdd.hAdd, LinearMap, RingHom.id, Matrix.GeneralLinearGroup.lieDeriv, Matrix.map, Complex.re, HSMul.hSMul, Complex.I, Complex.im
36 instances, coercions and auxiliary constants left out.
```
noncomputable def lieDerivC (Z : Matrix n n ℂ) : Module.End ℂ (smoothGL n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.smoothGL
lemma Matrix.GeneralLinearGroup.lieDerivC_add line 455 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Complex, Eq, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDerivC, HAdd.hAdd, RingHom.id
Proof uses: Eq.mpr, LinearMap, Matrix.GeneralLinearGroup.lieDeriv, Matrix.map, Complex.re, HSMul.hSMul, Complex.I, Complex.im, id, congrFun', congrArg, congr, Eq.trans, Matrix.GeneralLinearGroup.map_re_add, Matrix.GeneralLinearGroup.lieDeriv_add, Matrix.GeneralLinearGroup.map_im_add, smul_add
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivC_smul line 459 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, Matrix, Eq, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDerivC, HSMul.hSMul, RingHom.id
Proof uses: HAdd.hAdd, HMul.hMul, Complex.I, Eq.mpr, LinearMap, HSub.hSub, OfNat.ofNat, Matrix.GeneralLinearGroup.lieDeriv, Matrix.map, Complex.re, Complex.im, id, congrFun', congrArg, congr, Eq.trans, Matrix.GeneralLinearGroup.map_re_smul, Complex.mul_re, Complex.mul_im, Matrix.GeneralLinearGroup.lieDeriv_sub and 89 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.lieDerivC_bracket line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix, Complex, Eq, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.lieDerivC, HSub.hSub, HMul.hMul, RingHom.id
Proof uses: id, Eq.mpr, HAdd.hAdd, LinearMap, Matrix.GeneralLinearGroup.lieDeriv, Matrix.map, Complex.re, HSMul.hSMul, Complex.I, Complex.im, congrArg, Matrix.GeneralLinearGroup.map_re_bracket, Matrix.GeneralLinearGroup.map_im_bracket, Matrix.GeneralLinearGroup.lieDeriv_sub, Matrix.GeneralLinearGroup.lieDeriv_add, congr, Matrix.GeneralLinearGroup.lieDeriv_bracket, Eq.trans, smul_add, mul_add and 81 more
168 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.

FormalConjecturesForMathlib/NumberTheory/AutomorphicForm/BorelJacquet/LieDeriv.lean

Lie derivatives of smooth functions on GL n ℝ

Main declarations

Implementation notes

`FormalConjecturesForMathlib/NumberTheory/AutomorphicForm/BorelJacquet/LieDeriv.lean`

Lie derivatives of smooth functions on `GL n ℝ`