OAI/Analysis/CoulombIonization/FormDomain/WeakProduct.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CoulombAtom.smooth_lineDeriv_mulline 19 - lemma
OAI.CoulombAtom.IsWeakDerivative.mul_smoothline 31