OAI/NumberTheory/PiExponent/LocalAlgebra/WeightedLocalLattice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.WeightedLocalLattice.exists_local_element_iff_nonnegative_order line 12
2. def OAI.PiExponent.WeightedLocalLattice.generatedLattice line 48
3. theorem OAI.PiExponent.WeightedLocalLattice.generatedLattice_eq_span_of_minimum line 53
4. theorem OAI.PiExponent.WeightedLocalLattice.generatedLattice_rank_one_of_minimum line 81
5. def OAI.PiExponent.WeightedLocalLattice.monomialLattice line 90
6. theorem OAI.PiExponent.WeightedLocalLattice.exists_monomialLattice_generator line 95
7. theorem OAI.PiExponent.WeightedLocalLattice.monomialLattice_rank_one line 123