has_fderiv.mul in normed algebras ?

Stream: Is there code for X?

[Anatole Dedecker]

Do we really lack the following lemmas ? I only see lemmas about product in the field :/

import analysis.calculus.fderiv

variables {𝕂 𝔸 𝔸' 𝔼 : Type*} [nondiscrete_normed_field 𝕂] [normed_group 𝔼] [normed_space 𝕂 𝔼]
  [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [normed_comm_ring 𝔸'] [normed_algebra 𝕂 𝔸']
  {a b : 𝔼 → 𝔸} {a' b' : 𝔼 →L[𝕂] 𝔸} {c d : 𝔼 → 𝔸'} {c' d' : 𝔼 →L[𝕂] 𝔸'}

lemma has_strict_fderiv_at.mul' {x : 𝔼} (haa' : has_strict_fderiv_at a a' x) (hbb' : has_strict_fderiv_at b b' x) :
  has_strict_fderiv_at (a * b) (a x • b' + a'.smul_right (b x)) x :=
((continuous_linear_map.lmul 𝕂 𝔸).is_bounded_bilinear_map.has_strict_fderiv_at (a x, b x)).comp x
  (haa'.prod hbb')

-- Should replace the current `has_strict_fderiv_at.mul` ?
lemma has_strict_fderiv_at.mul'' {x : 𝔼} (hcc' : has_strict_fderiv_at c c' x)
  (hdd' : has_strict_fderiv_at d d' x) :
  has_strict_fderiv_at (c * d) (c x • d' + d x • c') x :=
by {convert hcc'.mul' hdd', ext z, apply mul_comm}

[Heather Macbeth]

I think it is, I remember noticing it before.

[Heather Macbeth]

In fact, this is most of what's missing to make units 𝔸 into a Lie group (and it shouldn't be very difficult).

[Heather Macbeth]

https://github.com/leanprover-community/mathlib/blob/9fc45d81e8d6eb7968e0c1c7aa3938044e4af61b/src/geometry/manifold/instances/units_of_normed_algebra.lean#L37