OAI/NumberTheory/Ostmann/Tree/AffineFibers.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.FiniteField.affinePair line 10
  2. def OAI.Ostmann.FiniteField.affineRatio line 13
  3. theorem OAI.Ostmann.FiniteField.affinePair_shift line 15
  4. theorem OAI.Ostmann.FiniteField.affineRatio_ne_zero line 20
  5. theorem OAI.Ostmann.FiniteField.affinePair_eq_identity_of_ratio_one line 23
  6. theorem OAI.Ostmann.FiniteField.affinePair_ratio_injective line 31
  7. theorem OAI.Ostmann.FiniteField.affinePair_fiber_card_le_two line 56
  8. def OAI.Ostmann.FiniteField.affineUnitSubstitution line 77
  9. def OAI.Ostmann.FiniteField.inverseAffineUnitSubstitution line 79
  10. theorem OAI.Ostmann.FiniteField.affineUnitSubstitution_inverse line 82
  11. theorem OAI.Ostmann.FiniteField.inverseAffineUnitSubstitution_affine line 88
  12. theorem OAI.Ostmann.FiniteField.affineUnitSubstitution_composition line 94