OAI/NumberTheory/PiExponent/Polynomials/FrameCoefficients.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Frames.O line 12
  2. def OAI.PiExponentSeshadri.Frames.endValue line 14
  3. lemma OAI.PiExponentSeshadri.Frames.end_apply line 16
  4. lemma OAI.PiExponentSeshadri.Frames.endValue_id line 22
  5. lemma OAI.PiExponentSeshadri.Frames.endValue_comp line 24
  6. def OAI.PiExponentSeshadri.Frames.frameChange line 28
  7. def OAI.PiExponentSeshadri.Frames.coefficient line 34
  8. lemma OAI.PiExponentSeshadri.Frames.coefficient_change line 37
  9. lemma OAI.PiExponentSeshadri.Frames.coefficient_frame line 43
  10. def OAI.PiExponentSeshadri.Frames.restrictSection line 46
  11. def OAI.PiExponentSeshadri.Frames.restrictFrame line 50
  12. lemma OAI.PiExponentSeshadri.Frames.end_naturality line 54
  13. lemma OAI.PiExponentSeshadri.Frames.endValue_restrict line 63
  14. lemma OAI.PiExponentSeshadri.Frames.coefficient_restrict line 78
  15. lemma OAI.PiExponentSeshadri.Frames.restrictUnit_comp line 88
  16. lemma OAI.PiExponentSeshadri.Frames.restrictSection_comp line 106
  17. lemma OAI.PiExponentSeshadri.Frames.coefficient_transport line 128
  18. lemma OAI.PiExponentSeshadri.Frames.coefficient_restrict_comp line 132
  19. lemma OAI.PiExponentSeshadri.Frames.restrictSection_congr line 142
  20. lemma OAI.PiExponentSeshadri.Frames.overlap_coefficients line 153