OAI/NumberTheory/PiExponent/LocalAlgebra/FlatLocalLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W25.simple_baseChange_of_map_maximalIdeal line 16
2. theorem OAI.PiExponentJets.W25.length_baseChange_of_flat_local line 35
3. theorem OAI.PiExponentJets.W25.finiteLength_baseChange_of_flat_local line 67
4. theorem OAI.PiExponentJets.W25.length_quotient_map_of_flat_local line 76