OAI/Geometry/TamingCompatibility/Hodge/HodgeGeometricGarding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeGeometricCoefficients.field line 20
  2. def OAI.TamingCompatibility.HodgeGeometricCoefficients.starredField line 22
  3. def OAI.TamingCompatibility.HodgeGeometricCoefficients.operator line 25
  4. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.starredField_eq line 30
  5. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.extDeriv_sum_zero line 35
  6. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.operator_system line 56
  7. theorem OAI.TamingCompatibility.HodgeGeometricCoefficients.geometric_local_garding line 90
  8. structure OAI.TamingCompatibility.HodgeChart.Data line 129
  9. theorem OAI.TamingCompatibility.HodgeChart.data_nonempty line 142
  10. def OAI.TamingCompatibility.HodgeChart.data line 173
  11. theorem OAI.TamingCompatibility.HodgeChart.finite_data_partition line 176