OAI/NumberTheory/PiExponent/Geometry/ProjectiveIntrinsicCoefficientLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData line 12
  2. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.chartOpen line 24
  3. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.Sections line 26
  4. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.Frame line 28
  5. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.frame line 32
  6. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.ringEquiv line 34
  7. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.polynomial line 37
  8. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.Law line 41
  9. theorem OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.CoordinateData.law line 45
  10. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsicData line 59
  11. def OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsicBundle line 68
  12. theorem OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsicBundle_sheaf line 71
  13. theorem OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsic_polynomial line 77
  14. theorem OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsic_ringEquiv line 81
  15. theorem OAI.PiExponent.ProjectiveIntrinsicCoefficientLaw.intrinsic_law line 88