PolynomialChartsAxiomAudit.lean

1 module
2 public import AffineObstructionCore
3 public import FiniteFiberCounts
4 public import PadicTowerLimit
5 public import PolynomialMinorSelection
6 public import PolynomialTaylor
7 public import ResidueLiftDigits
8 public import IntegerFiniteCokernel
9 public import PolynomialObstruction
10 public import PolynomialDigitBridge
11 public import PolynomialLiftCounts
12 public import PolynomialSurjectiveStep
13 public import PolynomialIntegerTower
14 public import PolynomialSmoothCounts
15 public import PolynomialTowerControls
16 public import PolynomialPadicLift
17 public import PolynomialCoefficientPerturbation
18 public import PolynomialPadicUnique
19 public import PolynomialParameterSystem
20 public import PolynomialCoordinateReorder
21 public import PolynomialInverseCongruence
22 public import PolynomialLocalSurjective
23 public import PolynomialRootStability
24 public import PolynomialLocalInverse
25 public import PolynomialParameterChart
26 public import PolynomialGeneralChart
27 public import PolynomialDeformationControls
28 public import PolynomialParameterControls
29 public import PolynomialCoefficientPerturbationContract
30 public import PolynomialGeneralChartContract
31 public import PolynomialHomeomorphContract
32 public import PolynomialLocalMapContract
33 public import PolynomialPadicUniqueContract
34 public import PolynomialRootStabilityContract
35 @[expose] public section
36 #print axioms Komorebi.FiniteFiberCounts.Fiber
37 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
38 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
39 #print axioms Komorebi.FiniteFiberCounts.difference
40 #print axioms Komorebi.FiniteFiberCounts.difference_translate
41 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
42 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
43 #print axioms Komorebi.FiniteFiberCounts.fiber_card
44 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
45 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
46 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
47 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
48 #print axioms Komorebi.FiniteFiberCounts.kernel_card
49 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
50 #print axioms Komorebi.FiniteFiberCounts.rank
51 #print axioms Komorebi.FiniteFiberCounts.translate
52 #print axioms Komorebi.FiniteFiberCounts.translate_add
53 #print axioms Komorebi.FiniteFiberCounts.translate_difference
54 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
55 #print axioms Komorebi.FiniteFiberCounts.translate_zero
56 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
57 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
58 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
59 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
60 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
61 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
62 #print axioms Komorebi.NativeAffine.Obstruction
63 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
64 #print axioms Komorebi.NativeAffine.affine_residual_transport
65 #print axioms Komorebi.NativeAffine.digitMap
66 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
67 #print axioms Komorebi.NativeAffine.obstruction
68 #print axioms Komorebi.NativeAffine.obstruction_finite
69 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
70 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
71 #print axioms Komorebi.NativeAffine.reduction
72 #print axioms Komorebi.NativeAffine.reduction_zero_iff
73 #print axioms Komorebi.NativeAffine.residual_exists
74 #print axioms Komorebi.NativeAffine.same_residue_iff
75 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
76 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
77 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit
78 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
79 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
80 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
81 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_eq
82 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_point_eq
83 #print axioms Komorebi.PolynomialCoefficientPerturbation.evalSystem_perturb
84 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_perturb
85 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_power_perturb
86 #print axioms Komorebi.PolynomialCoefficientPerturbation.lower_root_perturb
87 #print axioms Komorebi.PolynomialCoefficientPerturbation.padicEval_perturb
88 #print axioms Komorebi.PolynomialCoefficientPerturbation.pderiv_perturb
89 #print axioms Komorebi.PolynomialCoefficientPerturbation.perturb
90 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_perturbed_jacobian
91 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_power_perturbation_root
92 #print axioms Komorebi.PolynomialCoordinateReorder.continuous_reorderPoint
93 #print axioms Komorebi.PolynomialCoordinateReorder.digitJacobian_single
94 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder
95 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder_at
96 #print axioms Komorebi.PolynomialCoordinateReorder.exists_reorder_solvedJacobian_surjective
97 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder
98 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder_at
99 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_eval_reorder
100 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_reorder
101 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint
102 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse
103 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse'
104 #print axioms Komorebi.PolynomialCoordinateReorder.reorderSystem
105 #print axioms Komorebi.PolynomialCoordinateReorder.solvedJacobian_reorder_apply
106 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_coefficient_perturbation
107 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_no_extra_padic_precision
108 #print axioms Komorebi.PolynomialDeformationControls.squareMinusOne
109 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_jacobian_bijective
110 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_not_global_unique
111 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_two_padic_roots
112 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
113 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
114 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
115 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
116 #print axioms Komorebi.PolynomialDigitBridge.integerLift
117 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
118 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
119 #print axioms Komorebi.PolynomialGeneralChart.exists_parameter_homeomorph
120 #print axioms Komorebi.PolynomialGeneralChart.reorderRootHomeomorph
121 #print axioms Komorebi.PolynomialGeneralChartContract.full_rectangular_chart
122 #print axioms Komorebi.PolynomialHomeomorphContract.square_homeomorphism
123 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower
124 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong
125 #print axioms Komorebi.PolynomialIntegerTower.tower_digitJacobian_eq
126 #print axioms Komorebi.PolynomialIntegerTower.tower_initial_congruent
127 #print axioms Komorebi.PolynomialIntegerTower.tower_pairwise_congruent
128 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence
129 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence_step
130 #print axioms Komorebi.PolynomialInverseCongruence.padicEval_congruent
131 #print axioms Komorebi.PolynomialInverseCongruence.padic_congruence_iff
132 #print axioms Komorebi.PolynomialInverseCongruence.padic_inverse_congruence
133 #print axioms Komorebi.PolynomialInverseCongruence.padic_map_injective
134 #print axioms Komorebi.PolynomialLiftCounts.ActualLifts
135 #print axioms Komorebi.PolynomialLiftCounts.digitAddTorsor
136 #print axioms Komorebi.PolynomialLiftCounts.digitEquivLifts
137 #print axioms Komorebi.PolynomialLiftCounts.digit_residue_solution_iff
138 #print axioms Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count
139 #print axioms Komorebi.PolynomialLiftCounts.liftEquivKernel
140 #print axioms Komorebi.PolynomialLiftCounts.lift_card
141 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv
142 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv_class
143 #print axioms Komorebi.PolynomialLiftCounts.obstruction_card
144 #print axioms Komorebi.PolynomialLocalInverse.ballMap
145 #print axioms Komorebi.PolynomialLocalInverse.ballMap_bijective
146 #print axioms Komorebi.PolynomialLocalInverse.continuous_ballMap
147 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph
148 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_apply
149 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_congruent
150 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_eval
151 #print axioms Komorebi.PolynomialLocalMapContract.all_depths_reflected
152 #print axioms Komorebi.PolynomialLocalMapContract.arbitrary_padic_target
153 #print axioms Komorebi.PolynomialLocalSurjective.digitJacobian_sub_C
154 #print axioms Komorebi.PolynomialLocalSurjective.exists_integer_target_preimage
155 #print axioms Komorebi.PolynomialLocalSurjective.exists_padic_preimage
156 #print axioms Komorebi.PolynomialLocalSurjective.isClosed_residueBall
157 #print axioms Komorebi.PolynomialLocalSurjective.isCompact_residueBall
158 #print axioms Komorebi.PolynomialLocalSurjective.residueBall
159 #print axioms Komorebi.PolynomialLocalSurjective.truncInt_tendsto
160 #print axioms Komorebi.PolynomialMinorSelection.exists_permuted_columns
161 #print axioms Komorebi.PolynomialMinorSelection.exists_prime_permuted_columns
162 #print axioms Komorebi.PolynomialMinorSelection.exists_selected_columns
163 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
164 #print axioms Komorebi.PolynomialObstruction.evalSystem
165 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
166 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
167 #print axioms Komorebi.PolynomialObstruction.jacobian
168 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
169 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
170 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
171 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
172 #print axioms Komorebi.PolynomialObstruction.residual_exists
173 #print axioms Komorebi.PolynomialObstruction.residual_unique
174 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
175 #print axioms Komorebi.PolynomialPadicLift.continuous_padicEval
176 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root
177 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root_with_tower
178 #print axioms Komorebi.PolynomialPadicLift.padicEval
179 #print axioms Komorebi.PolynomialPadicLift.padicEval_intCast
180 #print axioms Komorebi.PolynomialPadicLift.polynomial_tower_limit_root
181 #print axioms Komorebi.PolynomialPadicUnique.exists_unique_padic_root
182 #print axioms Komorebi.PolynomialPadicUnique.int_pow_dvd_iff
183 #print axioms Komorebi.PolynomialPadicUnique.padic_root_unique
184 #print axioms Komorebi.PolynomialPadicUnique.rootResidueLift
185 #print axioms Komorebi.PolynomialPadicUnique.root_next_residue_eq
186 #print axioms Komorebi.PolynomialPadicUnique.toZModPow_eq_iff_dvd_sub
187 #print axioms Komorebi.PolynomialPadicUnique.truncInt
188 #print axioms Komorebi.PolynomialPadicUnique.truncInt_eval_residue
189 #print axioms Komorebi.PolynomialPadicUnique.truncInt_precision
190 #print axioms Komorebi.PolynomialPadicUnique.truncInt_root
191 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_arbitrary_root_uniqueness
192 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_unique_padic_root
193 #print axioms Komorebi.PolynomialParameterChart.chartGraph_iff
194 #print axioms Komorebi.PolynomialParameterChart.chartPhi
195 #print axioms Komorebi.PolynomialParameterChart.chartPoint
196 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent
197 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent_iff
198 #print axioms Komorebi.PolynomialParameterChart.chartPoint_free
199 #print axioms Komorebi.PolynomialParameterChart.chartPoint_graph
200 #print axioms Komorebi.PolynomialParameterChart.chartPoint_root
201 #print axioms Komorebi.PolynomialParameterChart.chartPoint_spec
202 #print axioms Komorebi.PolynomialParameterChart.chartPoint_unique
203 #print axioms Komorebi.PolynomialParameterChart.chartTarget
204 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPhi
205 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPoint
206 #print axioms Komorebi.PolynomialParameterChart.continuous_chartTarget
207 #print axioms Komorebi.PolynomialParameterChart.parameterHomeomorph
208 #print axioms Komorebi.PolynomialParameterControls.full_jacobian_surjective
209 #print axioms Komorebi.PolynomialParameterControls.no_root_at_parameter_two
210 #print axioms Komorebi.PolynomialParameterControls.parameter_two_near_origin
211 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_not_surjective
212 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_zero
213 #print axioms Komorebi.PolynomialParameterControls.squareMinusParameter
214 #print axioms Komorebi.PolynomialParameterSystem.augmented
215 #print axioms Komorebi.PolynomialParameterSystem.augmented_free
216 #print axioms Komorebi.PolynomialParameterSystem.augmented_jacobian_surjective
217 #print axioms Komorebi.PolynomialParameterSystem.augmented_solved
218 #print axioms Komorebi.PolynomialParameterSystem.continuous_freePart
219 #print axioms Komorebi.PolynomialParameterSystem.continuous_join
220 #print axioms Komorebi.PolynomialParameterSystem.continuous_solvedPart
221 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_augmented
222 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_join_zero
223 #print axioms Komorebi.PolynomialParameterSystem.evalSystem_augmented
224 #print axioms Komorebi.PolynomialParameterSystem.freePart
225 #print axioms Komorebi.PolynomialParameterSystem.freePart_join
226 #print axioms Komorebi.PolynomialParameterSystem.join
227 #print axioms Komorebi.PolynomialParameterSystem.join_free
228 #print axioms Komorebi.PolynomialParameterSystem.join_parts
229 #print axioms Komorebi.PolynomialParameterSystem.join_solved
230 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented
231 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented_iff
232 #print axioms Komorebi.PolynomialParameterSystem.solvedJacobian
233 #print axioms Komorebi.PolynomialParameterSystem.solvedPart
234 #print axioms Komorebi.PolynomialParameterSystem.solvedPart_join
235 #print axioms Komorebi.PolynomialRootStability.exists_nearby_perturbed_root
236 #print axioms Komorebi.PolynomialRootStability.exists_root_and_unique_perturbation
237 #print axioms Komorebi.PolynomialRootStability.exists_unique_nearby_perturbed_root
238 #print axioms Komorebi.PolynomialRootStability.integer_congruent_of_common_padic
239 #print axioms Komorebi.PolynomialRootStability.perturbed_roots_congruent
240 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_lower_root_and_unique_perturbation
241 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_rectangular_nearby_root
242 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_square_root_displacement
243 #print axioms Komorebi.PolynomialSmoothCounts.exists_regular_tower
244 #print axioms Komorebi.PolynomialSmoothCounts.smooth_dimension
245 #print axioms Komorebi.PolynomialSmoothCounts.smooth_lift_card
246 #print axioms Komorebi.PolynomialSmoothCounts.smooth_obstruction_card
247 #print axioms Komorebi.PolynomialSmoothCounts.smooth_rank
248 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_eq
249 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_shift_eq
250 #print axioms Komorebi.PolynomialSurjectiveStep.one_step_lift
251 #print axioms Komorebi.PolynomialTaylor.directional
252 #print axioms Komorebi.PolynomialTaylor.directional_C
253 #print axioms Komorebi.PolynomialTaylor.directional_X
254 #print axioms Komorebi.PolynomialTaylor.directional_add
255 #print axioms Komorebi.PolynomialTaylor.directional_mul
256 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
257 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
258 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
259 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
260 #print axioms Komorebi.PolynomialTowerControls.linearMinusTwo
261 #print axioms Komorebi.PolynomialTowerControls.linear_shift_no_extra_precision
262 #print axioms Komorebi.PolynomialTowerControls.linear_shift_nonsingular_lower_root
263 #print axioms Komorebi.PolynomialTowerControls.projectionSystem
264 #print axioms Komorebi.PolynomialTowerControls.projection_jacobian_surjective
265 #print axioms Komorebi.PolynomialTowerControls.projection_two_padic_roots
266 #print axioms Komorebi.PolynomialTowerControls.squareMinusFive
267 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_lower_steps
268 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_mod_eight
269 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_tower
270 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
271 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
272 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
273 #print axioms Komorebi.ResidueLiftDigits.digitResidue
274 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
275 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
276 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
277 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
278 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
279 #print axioms Komorebi.ResidueLiftDigits.shift_cast_eq_iff

Back to source controls