OAI/NumberTheory/PiExponent/LocalAlgebra/ParameterKilledFiniteLength.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W06.isArtinianRing_quotient_parameter line 11
2. theorem OAI.PiExponentJets.W06.isFiniteLength_of_parameter_killed line 21
3. theorem OAI.PiExponentJets.W06.length_ne_top_of_parameter_killed line 38
4. theorem OAI.PiExponentJets.W06.parameter_kills_mul_kernel line 45
5. theorem OAI.PiExponentJets.W06.parameter_kills_mul_cokernel line 54
6. theorem OAI.PiExponentJets.W06.isFiniteLength_ker_parameter_mul line 61
7. theorem OAI.PiExponentJets.W06.isFiniteLength_coker_parameter_mul line 68
8. theorem OAI.PiExponentJets.W06.kernel_cokernel_parameter_lengths_ne_top line 73