OAI/NumberTheory/Ostmann/Characters/SymbolicHistory.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.Characters.SymbolicHistory.Expr line 9
  2. theorem OAI.Ostmann.Characters.SymbolicHistory.Expr.rational_castHom_apply line 20
  3. def OAI.Ostmann.Characters.SymbolicHistory.Expr.denominator line 22
  4. def OAI.Ostmann.Characters.SymbolicHistory.Expr.numerator line 30
  5. def OAI.Ostmann.Characters.SymbolicHistory.Expr.Valid line 38
  6. def OAI.Ostmann.Characters.SymbolicHistory.Expr.rationalEval line 46
  7. def OAI.Ostmann.Characters.SymbolicHistory.Expr.integerEval line 54
  8. def OAI.Ostmann.Characters.SymbolicHistory.Expr.IntegralAt line 62
  9. theorem OAI.Ostmann.Characters.SymbolicHistory.Expr.denominator_ne_zero line 70
  10. theorem OAI.Ostmann.Characters.SymbolicHistory.Expr.rationalEval_eq line 79
  11. theorem OAI.Ostmann.Characters.SymbolicHistory.Expr.integerEval_cleared line 105
  12. def OAI.Ostmann.Characters.SymbolicHistory.Expr.degreeBudget line 127
  13. theorem OAI.Ostmann.Characters.SymbolicHistory.Expr.numerator_degree_le line 135