OAI/Geometry/IntegralFillings/Charts/Reparametrization.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpIntegralFillings.IntegerChart.reparamline 38 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_scalarline 71 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_imageline 80 - lemma
OAI.SharpIntegralFillings.row_det_compline 94 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_jacobian_aeline 116 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_actionline 142 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_isMetricCurrentline 159 - lemma
OAI.SharpIntegralFillings.IntegerChart.reparam_massline 164