OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedTerminalIntegerPriorProperties.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerSupport_eq_nat_imageline 20 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceNaturalSupport_primeline 25 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerSupport_positive_primeline 30 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight_nonnegline 34 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight_pos_iffline 38 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight_eq_zero_of_not_memline 42 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerWeight_sumline 46 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerSupport_boundsline 50 - theorem
OAI.Ostmann.Characters.TemplateOneSidedTerminalSupportRemoval.terminalSourceIntegerSupport_abs_leline 57