OAI/NumberTheory/PiExponent/Approximation/RegularSectionChoice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.NumericalAmpleness.finite_affine_frame_cover line 15
2. theorem OAI.PiExponent.NumericalAmpleness.coefficients_span_top_of_section_cover line 41
3. def OAI.PiExponent.NumericalAmpleness.localCoefficientAddHom line 57
4. theorem OAI.PiExponent.NumericalAmpleness.iso_inv_map_comp line 69
5. theorem OAI.PiExponent.NumericalAmpleness.localCoefficient_scalar line 74
6. def OAI.PiExponent.NumericalAmpleness.sectionLinearCombination line 93
7. theorem OAI.PiExponent.NumericalAmpleness.localCoefficient_linearCombination line 97
8. theorem OAI.PiExponent.NumericalAmpleness.exists_mono_linearCombination_of_finite_cover line 108
9. theorem OAI.PiExponent.NumericalAmpleness.exists_mono_section_of_finite_cover line 132