OAI/Geometry/NodalSets/Charts/CircleChartFactor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.Target.CircleModel line 9
  2. def OAI.Yau.Target.circleChartDerivative line 11
  3. def OAI.Yau.Target.circleChartFactor line 16
  4. lemma OAI.Yau.Target.circleChartDerivative_injective line 19
  5. lemma OAI.Yau.Target.circleChartFactor_pos line 27
  6. lemma OAI.Yau.Target.circleChartDerivative_inner_basis line 35