OAI/NumberTheory/PiExponent/LocalAlgebra/RegularParameterSelection2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W58.regular_full_length_radical_eq_maximalIdeal line 14
2. theorem OAI.PiExponentSiegel.W58.constant_linearCombination_mem_ideal line 40
3. theorem OAI.PiExponentSiegel.W58.exists_constant_regular_parameters_of_no_maximal_associated line 49