OAI/Algebra/FiniteTensor/NormalResidues.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normal-cycle residues, restricted gradients and nonzero exterior pairings.

  1. theorem OAI.PD4Tensor.Forms.normalCycle_product line 19
  2. theorem OAI.PD4Tensor.Forms.topCoefficient_normalCycle line 34
  3. theorem OAI.PD4Tensor.FrobeniusTruncation.exterior_normal_residue line 58
  4. theorem OAI.PD4Tensor.FrobeniusTruncation.exterior_normal_residue_ne_zero line 75
  5. theorem OAI.PD4Tensor.Forms.restricted_gradient_boundary line 96
  6. theorem OAI.PD4Tensor.FrobeniusTruncation.inverse_normal_residue_ne_zero line 124
  7. theorem OAI.PD4Tensor.Forms.normalCycle_append line 143