OAI/Analysis/BiholderTransport/LinearAlgebra/Diagonal.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.diagonal_stationary_hessian_identityline 18 - lemma
OAI.WeakMTWTransport.diagonalSplitAction_hessian_identityline 47 - lemma
OAI.WeakMTWTransport.exists_suffix_log_in_prefix_coordinatesline 60