OAI/Analysis/VlasovMaxwell/Population/DirectExpandedDeficitUniform.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.direct_remaining_source_deficit_short_uniform_expanded line 12