OAI/NumberTheory/Ostmann/Characters/HigherBiasSourceTargetsAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.HigherBiasSourceTargets.targetTail line 9
  2. def OAI.Ostmann.Characters.HigherBiasSourceTargets.target line 12
  3. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.targetTail_end line 15
  4. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.targetTail_step line 17
  5. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_eq line 29
  6. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.sum_target line 34
  7. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_recurrence line 39
  8. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_total line 43
  9. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.targetTail_nonneg line 48
  10. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_nonneg line 54
  11. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_le_total line 59
  12. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.target_ge_last line 64