OAI/NumberTheory/Ostmann/Arithmetic/HistoryFieldEvaluation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.RationalHistory.Expr.fieldEval line 10
  2. def OAI.Ostmann.Characters.RationalHistory.Expr.FieldRegularAt line 18
  3. theorem OAI.Ostmann.Characters.RationalHistory.Expr.field_cast_apply line 26
  4. theorem OAI.Ostmann.Characters.RationalHistory.Expr.field_cleared line 28
  5. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fieldEval_eq line 67