OAI/NumberTheory/PiExponent/Jets/BranchContactIdeal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.BranchContactIdeal.powerIdeal line 12
2. theorem OAI.PiExponent.BranchContactIdeal.powerIdeal_eq_singleton line 15
3. theorem OAI.PiExponent.BranchContactIdeal.addVal_pow_toNat line 27
4. def OAI.PiExponent.BranchContactIdeal.contact line 36
5. theorem OAI.PiExponent.BranchContactIdeal.exists_generator_colength_eq_contact line 41
6. theorem OAI.PiExponent.BranchContactIdeal.colength_eq_contact line 89