OAI/Geometry/PrescribedRicci/CofactorBilin.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cofactor Bilin.

  1. def OAI.GlobalElliptic.cofactorBilinLinear line 21
  2. def OAI.GlobalElliptic.cofactorBilin line 32
  3. lemma OAI.GlobalElliptic.cofactorBilin_apply line 37
  4. lemma OAI.GlobalElliptic.cofactorBilin_expansion line 40
  5. lemma OAI.GlobalElliptic.cofactor_smooth_expression line 53