OAI/Analysis/Conductivity/Flux/AttachedFlatTensor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.attachedCartesianMatrix line 12
  2. lemma OAI.ScalarConductivity.attachedCartesianMatrix_det_ne_zero line 15
  3. def OAI.ScalarConductivity.attachedFlatTensor line 22
  4. lemma OAI.ScalarConductivity.attachedFlatTensor_symmetric line 28
  5. lemma OAI.ScalarConductivity.attachedFlatTensor_energy line 33
  6. lemma OAI.ScalarConductivity.attachedFlatTensor_energy_density line 40
  7. lemma OAI.ScalarConductivity.flat_inverse_congruence_positive line 49
  8. lemma OAI.ScalarConductivity.continuousOn_attachedCartesianMatrix line 76
  9. lemma OAI.ScalarConductivity.continuousOn_attachedFlatTensor line 80
  10. theorem OAI.ScalarConductivity.attachedFlatTensor_elliptic line 95
  11. lemma OAI.ScalarConductivity.attachedCartesianMatrix_poisson_derivative line 106