PolynomialRegularityAxiomAudit.lean

1 module
2 public import AffineObstructionCore
3 public import FiniteFiberCounts
4 public import PadicTowerLimit
5 public import PolynomialAnalyticInverse
6 public import PolynomialMinorSelection
7 public import PolynomialPadicContraction
8 public import PolynomialTaylor
9 public import PolynomialTaylorRing
10 public import PolynomialWeightedInverse
11 public import ResidueLiftDigits
12 public import IntegerFiniteCokernel
13 public import PolynomialAnalyticEvaluation
14 public import PolynomialMotionRational
15 public import PolynomialObstruction
16 public import PolynomialTaylorDisplacement
17 public import PolynomialWeightedNormalization
18 public import PolynomialDigitBridge
19 public import PolynomialMotionEstimate
20 public import PolynomialMotionNormalization
21 public import PolynomialWeightedLift
22 public import PolynomialLiftCounts
23 public import PolynomialRootMotion
24 public import PolynomialSurjectiveStep
25 public import PolynomialIntegerTower
26 public import PolynomialSmoothCounts
27 public import PolynomialTowerControls
28 public import PolynomialPadicLift
29 public import PolynomialCoefficientPerturbation
30 public import PolynomialPadicUnique
31 public import PolynomialParameterSystem
32 public import PolynomialBlockInverse
33 public import PolynomialCoordinateReorder
34 public import PolynomialInverseCongruence
35 public import PolynomialLocalSurjective
36 public import PolynomialParameterPath
37 public import PolynomialPrescribedSystem
38 public import PolynomialRootStability
39 public import PolynomialAnalyticBlocks
40 public import PolynomialJointSystem
41 public import PolynomialLocalInverse
42 public import PolynomialPrescribedLifts
43 public import PolynomialPrescribedTowerLimit
44 public import PolynomialAnalyticImplicit
45 public import PolynomialJointMotion
46 public import PolynomialParameterChart
47 public import PolynomialPrescribedCounts
48 public import PolynomialAnalyticSelection
49 public import PolynomialGeneralChart
50 public import PolynomialJointDeformation
51 public import PolynomialPrescribedObstruction
52 public import PolynomialPrescribedStep
53 public import PolynomialPrescribedTowerUnique
54 public import PolynomialRegularityIntegral
55 public import PolynomialPrescribedIntegerTower
56 public import PolynomialPrescribedPadicTower
57 public import PolynomialDeformationControls
58 public import PolynomialParameterControls
59 public import PolynomialParameterTowerControls
60 public import PolynomialPrescribedControls
61 public import PolynomialRegularityControls
62 public import PolynomialWeightedControls
63 public import PolynomialMotionControls
64 public import PolynomialJointMotionControls
65 public import PolynomialCoefficientPerturbationContract
66 public import PolynomialGeneralChartContract
67 public import PolynomialHomeomorphContract
68 public import PolynomialJointMotionContracts
69 public import PolynomialLocalMapContract
70 public import PolynomialPadicUniqueContract
71 public import PolynomialPrescribedContract
72 public import PolynomialRegularityContracts
73 public import PolynomialRootMotionContract
74 public import PolynomialRootStabilityContract
75 public import PolynomialWeightedAuxiliaryContract
76 public import PolynomialWeightedLiftContract
77 public import PolynomialParameterTowerContracts
78 @[expose] public section
79 #print axioms Komorebi.FiniteFiberCounts.Fiber
80 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
81 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
82 #print axioms Komorebi.FiniteFiberCounts.difference
83 #print axioms Komorebi.FiniteFiberCounts.difference_translate
84 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
85 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
86 #print axioms Komorebi.FiniteFiberCounts.fiber_card
87 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
88 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
89 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
90 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
91 #print axioms Komorebi.FiniteFiberCounts.kernel_card
92 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
93 #print axioms Komorebi.FiniteFiberCounts.rank
94 #print axioms Komorebi.FiniteFiberCounts.translate
95 #print axioms Komorebi.FiniteFiberCounts.translate_add
96 #print axioms Komorebi.FiniteFiberCounts.translate_difference
97 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
98 #print axioms Komorebi.FiniteFiberCounts.translate_zero
99 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
100 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
101 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
102 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
103 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
104 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
105 #print axioms Komorebi.NativeAffine.Obstruction
106 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
107 #print axioms Komorebi.NativeAffine.affine_residual_transport
108 #print axioms Komorebi.NativeAffine.digitMap
109 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
110 #print axioms Komorebi.NativeAffine.obstruction
111 #print axioms Komorebi.NativeAffine.obstruction_finite
112 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
113 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
114 #print axioms Komorebi.NativeAffine.reduction
115 #print axioms Komorebi.NativeAffine.reduction_zero_iff
116 #print axioms Komorebi.NativeAffine.residual_exists
117 #print axioms Komorebi.NativeAffine.same_residue_iff
118 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
119 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
120 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit
121 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
122 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
123 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
124 #print axioms Komorebi.PolynomialAnalyticBlocks.inverse_free_zero
125 #print axioms Komorebi.PolynomialAnalyticBlocks.inverse_solved_zero
126 #print axioms Komorebi.PolynomialAnalyticBlocks.upperEquiv
127 #print axioms Komorebi.PolynomialAnalyticBlocks.upperEquiv_apply
128 #print axioms Komorebi.PolynomialAnalyticBlocks.upperEquiv_symm_apply
129 #print axioms Komorebi.PolynomialAnalyticBlocks.upperEquiv_toCLM
130 #print axioms Komorebi.PolynomialAnalyticEvaluation.analyticAt_evalSystem
131 #print axioms Komorebi.PolynomialAnalyticEvaluation.analyticOnNhd_evalSystem
132 #print axioms Komorebi.PolynomialAnalyticEvaluation.evalSystem
133 #print axioms Komorebi.PolynomialAnalyticEvaluation.hasStrictFDerivAt_eval
134 #print axioms Komorebi.PolynomialAnalyticEvaluation.hasStrictFDerivAt_evalSystem
135 #print axioms Komorebi.PolynomialAnalyticEvaluation.matrixCLM
136 #print axioms Komorebi.PolynomialAnalyticEvaluation.matrixCLM_apply
137 #print axioms Komorebi.PolynomialAnalyticEvaluation.polynomialDeriv
138 #print axioms Komorebi.PolynomialAnalyticEvaluation.polynomialDeriv_apply
139 #print axioms Komorebi.PolynomialAnalyticImplicit.differentiableOn_of_analytic_graph
140 #print axioms Komorebi.PolynomialAnalyticImplicit.exists_analytic_graph
141 #print axioms Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit
142 #print axioms Komorebi.PolynomialAnalyticImplicit.parameterInjectionCLM
143 #print axioms Komorebi.PolynomialAnalyticImplicit.parameterInjectionCLM_apply
144 #print axioms Komorebi.PolynomialAnalyticImplicit.solvedPartCLM
145 #print axioms Komorebi.PolynomialAnalyticImplicit.solvedPartCLM_apply
146 #print axioms Komorebi.PolynomialAnalyticInverse.analyticAt_inverse
147 #print axioms Komorebi.PolynomialAnalyticInverse.exists_open_analytic_inverse
148 #print axioms Komorebi.PolynomialAnalyticSelection.continuous_selection_analyticOnNhd
149 #print axioms Komorebi.PolynomialAnalyticSelection.continuous_selection_eventually_eq
150 #print axioms Komorebi.PolynomialAnalyticSelection.continuous_selection_regularity
151 #print axioms Komorebi.PolynomialBlockInverse.blockCertificate
152 #print axioms Komorebi.PolynomialBlockInverse.blockCertificate_mul
153 #print axioms Komorebi.PolynomialBlockInverse.blockCertificate_mulVec_join_neg
154 #print axioms Komorebi.PolynomialBlockInverse.blockCertificate_two_sided
155 #print axioms Komorebi.PolynomialBlockInverse.bounded_inverse_upperBlock
156 #print axioms Komorebi.PolynomialBlockInverse.mul_blockCertificate
157 #print axioms Komorebi.PolynomialBlockInverse.upperBlock
158 #print axioms Komorebi.PolynomialBlockInverse.upperBlock_free_free
159 #print axioms Komorebi.PolynomialBlockInverse.upperBlock_free_solved
160 #print axioms Komorebi.PolynomialBlockInverse.upperBlock_mulVec_join
161 #print axioms Komorebi.PolynomialBlockInverse.upperBlock_solved_free
162 #print axioms Komorebi.PolynomialBlockInverse.upperBlock_solved_solved
163 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_eq
164 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_point_eq
165 #print axioms Komorebi.PolynomialCoefficientPerturbation.evalSystem_perturb
166 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_perturb
167 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_power_perturb
168 #print axioms Komorebi.PolynomialCoefficientPerturbation.lower_root_perturb
169 #print axioms Komorebi.PolynomialCoefficientPerturbation.padicEval_perturb
170 #print axioms Komorebi.PolynomialCoefficientPerturbation.pderiv_perturb
171 #print axioms Komorebi.PolynomialCoefficientPerturbation.perturb
172 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_perturbed_jacobian
173 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_power_perturbation_root
174 #print axioms Komorebi.PolynomialCoordinateReorder.continuous_reorderPoint
175 #print axioms Komorebi.PolynomialCoordinateReorder.digitJacobian_single
176 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder
177 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder_at
178 #print axioms Komorebi.PolynomialCoordinateReorder.exists_reorder_solvedJacobian_surjective
179 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder
180 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder_at
181 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_eval_reorder
182 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_reorder
183 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint
184 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse
185 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse'
186 #print axioms Komorebi.PolynomialCoordinateReorder.reorderSystem
187 #print axioms Komorebi.PolynomialCoordinateReorder.solvedJacobian_reorder_apply
188 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_coefficient_perturbation
189 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_no_extra_padic_precision
190 #print axioms Komorebi.PolynomialDeformationControls.squareMinusOne
191 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_jacobian_bijective
192 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_not_global_unique
193 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_two_padic_roots
194 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
195 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
196 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
197 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
198 #print axioms Komorebi.PolynomialDigitBridge.integerLift
199 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
200 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
201 #print axioms Komorebi.PolynomialGeneralChart.exists_parameter_homeomorph
202 #print axioms Komorebi.PolynomialGeneralChart.reorderRootHomeomorph
203 #print axioms Komorebi.PolynomialGeneralChartContract.full_rectangular_chart
204 #print axioms Komorebi.PolynomialHomeomorphContract.square_homeomorphism
205 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower
206 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong
207 #print axioms Komorebi.PolynomialIntegerTower.tower_digitJacobian_eq
208 #print axioms Komorebi.PolynomialIntegerTower.tower_initial_congruent
209 #print axioms Komorebi.PolynomialIntegerTower.tower_pairwise_congruent
210 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence
211 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence_step
212 #print axioms Komorebi.PolynomialInverseCongruence.padicEval_congruent
213 #print axioms Komorebi.PolynomialInverseCongruence.padic_congruence_iff
214 #print axioms Komorebi.PolynomialInverseCongruence.padic_inverse_congruence
215 #print axioms Komorebi.PolynomialInverseCongruence.padic_map_injective
216 #print axioms Komorebi.PolynomialJointDeformation.exists_joint_deformation
217 #print axioms Komorebi.PolynomialJointDeformation.exists_unique_joint_deformation
218 #print axioms Komorebi.PolynomialJointDeformation.join_deformed_ball
219 #print axioms Komorebi.PolynomialJointMotion.exists_joint_root_certificate
220 #print axioms Komorebi.PolynomialJointMotion.exists_joint_root_motion
221 #print axioms Komorebi.PolynomialJointMotionContracts.actual_joint_certificate
222 #print axioms Komorebi.PolynomialJointMotionContracts.actual_joint_rational_motion
223 #print axioms Komorebi.PolynomialJointMotionControls.exists_sharp_parameter_only_root
224 #print axioms Komorebi.PolynomialJointMotionControls.join_one_one
225 #print axioms Komorebi.PolynomialJointMotionControls.join_one_zero
226 #print axioms Komorebi.PolynomialJointMotionControls.linearPerturbation
227 #print axioms Komorebi.PolynomialJointMotionControls.linearSystem
228 #print axioms Komorebi.PolynomialJointMotionControls.linear_actual_jacobians
229 #print axioms Komorebi.PolynomialJointMotionControls.linear_augmented_root_depth_two
230 #print axioms Komorebi.PolynomialJointMotionControls.linear_base_data
231 #print axioms Komorebi.PolynomialJointMotionControls.linear_joint_forcing_and_error
232 #print axioms Komorebi.PolynomialJointMotionControls.linear_joint_root
233 #print axioms Komorebi.PolynomialJointMotionControls.linear_joint_unique
234 #print axioms Komorebi.PolynomialJointMotionControls.no_uniform_extra_parameter_error_digit
235 #print axioms Komorebi.PolynomialJointMotionControls.omitted_parameter_term_fails
236 #print axioms Komorebi.PolynomialJointMotionControls.quadraticParameterSystem
237 #print axioms Komorebi.PolynomialJointMotionControls.quadratic_parameter_base_data
238 #print axioms Komorebi.PolynomialJointMotionControls.reversed_parameter_sign_fails
239 #print axioms Komorebi.PolynomialJointSystem.augmented
240 #print axioms Komorebi.PolynomialJointSystem.augmentedPerturbation
241 #print axioms Komorebi.PolynomialJointSystem.augmentedPerturbation_free
242 #print axioms Komorebi.PolynomialJointSystem.augmentedPerturbation_solved
243 #print axioms Komorebi.PolynomialJointSystem.augmented_free
244 #print axioms Komorebi.PolynomialJointSystem.augmented_root
245 #print axioms Komorebi.PolynomialJointSystem.augmented_solved
246 #print axioms Komorebi.PolynomialJointSystem.eval_augmented
247 #print axioms Komorebi.PolynomialJointSystem.eval_augmentedPerturbation
248 #print axioms Komorebi.PolynomialJointSystem.jacobian_augmented
249 #print axioms Komorebi.PolynomialJointSystem.jacobian_augmented_free_free
250 #print axioms Komorebi.PolynomialJointSystem.jacobian_augmented_free_solved
251 #print axioms Komorebi.PolynomialJointSystem.jacobian_augmented_solved_free
252 #print axioms Komorebi.PolynomialJointSystem.jacobian_augmented_solved_solved
253 #print axioms Komorebi.PolynomialJointSystem.parameterJacobian
254 #print axioms Komorebi.PolynomialJointSystem.perturb_augmented_root_iff
255 #print axioms Komorebi.PolynomialJointSystem.solvedJacobian
256 #print axioms Komorebi.PolynomialLiftCounts.ActualLifts
257 #print axioms Komorebi.PolynomialLiftCounts.digitAddTorsor
258 #print axioms Komorebi.PolynomialLiftCounts.digitEquivLifts
259 #print axioms Komorebi.PolynomialLiftCounts.digit_residue_solution_iff
260 #print axioms Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count
261 #print axioms Komorebi.PolynomialLiftCounts.liftEquivKernel
262 #print axioms Komorebi.PolynomialLiftCounts.lift_card
263 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv
264 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv_class
265 #print axioms Komorebi.PolynomialLiftCounts.obstruction_card
266 #print axioms Komorebi.PolynomialLocalInverse.ballMap
267 #print axioms Komorebi.PolynomialLocalInverse.ballMap_bijective
268 #print axioms Komorebi.PolynomialLocalInverse.continuous_ballMap
269 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph
270 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_apply
271 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_congruent
272 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_eval
273 #print axioms Komorebi.PolynomialLocalMapContract.all_depths_reflected
274 #print axioms Komorebi.PolynomialLocalMapContract.arbitrary_padic_target
275 #print axioms Komorebi.PolynomialLocalSurjective.digitJacobian_sub_C
276 #print axioms Komorebi.PolynomialLocalSurjective.exists_integer_target_preimage
277 #print axioms Komorebi.PolynomialLocalSurjective.exists_padic_preimage
278 #print axioms Komorebi.PolynomialLocalSurjective.isClosed_residueBall
279 #print axioms Komorebi.PolynomialLocalSurjective.isCompact_residueBall
280 #print axioms Komorebi.PolynomialLocalSurjective.residueBall
281 #print axioms Komorebi.PolynomialLocalSurjective.truncInt_tendsto
282 #print axioms Komorebi.PolynomialMinorSelection.exists_permuted_columns
283 #print axioms Komorebi.PolynomialMinorSelection.exists_prime_permuted_columns
284 #print axioms Komorebi.PolynomialMinorSelection.exists_selected_columns
285 #print axioms Komorebi.PolynomialMotionControls.exists_sharp_motion_root
286 #print axioms Komorebi.PolynomialMotionControls.no_uniform_extra_error_digit
287 #print axioms Komorebi.PolynomialMotionControls.sharpQuadratic
288 #print axioms Komorebi.PolynomialMotionControls.sharpQuadratic_base
289 #print axioms Komorebi.PolynomialMotionControls.sharp_error_of_even_root
290 #print axioms Komorebi.PolynomialMotionControls.sharp_mod_eight
291 #print axioms Komorebi.PolynomialMotionEstimate.first_order_error_dvd
292 #print axioms Komorebi.PolynomialMotionNormalization.eval_perturbSystem
293 #print axioms Komorebi.PolynomialMotionNormalization.exists_eval_scaled_difference
294 #print axioms Komorebi.PolynomialMotionNormalization.exists_motion_normalization
295 #print axioms Komorebi.PolynomialMotionNormalization.perturbSystem
296 #print axioms Komorebi.PolynomialMotionNormalization.precondition_perturbSystem
297 #print axioms Komorebi.PolynomialMotionRational.coe_mulVec
298 #print axioms Komorebi.PolynomialMotionRational.exists_rational_error
299 #print axioms Komorebi.PolynomialMotionRational.scaled_inverse_mulVec
300 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
301 #print axioms Komorebi.PolynomialObstruction.evalSystem
302 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
303 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
304 #print axioms Komorebi.PolynomialObstruction.jacobian
305 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
306 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
307 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
308 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
309 #print axioms Komorebi.PolynomialObstruction.residual_exists
310 #print axioms Komorebi.PolynomialObstruction.residual_unique
311 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
312 #print axioms Komorebi.PolynomialPadicContraction.contracting_contractionMap
313 #print axioms Komorebi.PolynomialPadicContraction.contractionMap
314 #print axioms Komorebi.PolynomialPadicContraction.evalSystem
315 #print axioms Komorebi.PolynomialPadicContraction.eval_dist_le
316 #print axioms Komorebi.PolynomialPadicContraction.eval_dvd_of_dvd
317 #print axioms Komorebi.PolynomialPadicContraction.exists_unique_fixedPoint
318 #print axioms Komorebi.PolynomialPadicContraction.exists_unique_fixedPoint_divisible
319 #print axioms Komorebi.PolynomialPadicContraction.fixedPoint_divisible
320 #print axioms Komorebi.PolynomialPadicContraction.lipschitz_evalSystem
321 #print axioms Komorebi.PolynomialPadicLift.continuous_padicEval
322 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root
323 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root_with_tower
324 #print axioms Komorebi.PolynomialPadicLift.padicEval
325 #print axioms Komorebi.PolynomialPadicLift.padicEval_intCast
326 #print axioms Komorebi.PolynomialPadicLift.polynomial_tower_limit_root
327 #print axioms Komorebi.PolynomialPadicUnique.exists_unique_padic_root
328 #print axioms Komorebi.PolynomialPadicUnique.int_pow_dvd_iff
329 #print axioms Komorebi.PolynomialPadicUnique.padic_root_unique
330 #print axioms Komorebi.PolynomialPadicUnique.rootResidueLift
331 #print axioms Komorebi.PolynomialPadicUnique.root_next_residue_eq
332 #print axioms Komorebi.PolynomialPadicUnique.toZModPow_eq_iff_dvd_sub
333 #print axioms Komorebi.PolynomialPadicUnique.truncInt
334 #print axioms Komorebi.PolynomialPadicUnique.truncInt_eval_residue
335 #print axioms Komorebi.PolynomialPadicUnique.truncInt_precision
336 #print axioms Komorebi.PolynomialPadicUnique.truncInt_root
337 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_arbitrary_root_uniqueness
338 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_unique_padic_root
339 #print axioms Komorebi.PolynomialParameterChart.chartGraph_iff
340 #print axioms Komorebi.PolynomialParameterChart.chartPhi
341 #print axioms Komorebi.PolynomialParameterChart.chartPoint
342 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent
343 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent_iff
344 #print axioms Komorebi.PolynomialParameterChart.chartPoint_free
345 #print axioms Komorebi.PolynomialParameterChart.chartPoint_graph
346 #print axioms Komorebi.PolynomialParameterChart.chartPoint_root
347 #print axioms Komorebi.PolynomialParameterChart.chartPoint_spec
348 #print axioms Komorebi.PolynomialParameterChart.chartPoint_unique
349 #print axioms Komorebi.PolynomialParameterChart.chartTarget
350 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPhi
351 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPoint
352 #print axioms Komorebi.PolynomialParameterChart.continuous_chartTarget
353 #print axioms Komorebi.PolynomialParameterChart.parameterHomeomorph
354 #print axioms Komorebi.PolynomialParameterControls.full_jacobian_surjective
355 #print axioms Komorebi.PolynomialParameterControls.no_root_at_parameter_two
356 #print axioms Komorebi.PolynomialParameterControls.parameter_two_near_origin
357 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_not_surjective
358 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_zero
359 #print axioms Komorebi.PolynomialParameterControls.squareMinusParameter
360 #print axioms Komorebi.PolynomialParameterPath.exists_parameter_path
361 #print axioms Komorebi.PolynomialParameterPath.parameterPath
362 #print axioms Komorebi.PolynomialParameterPath.parameterPath_compatible
363 #print axioms Komorebi.PolynomialParameterPath.parameterPath_precision
364 #print axioms Komorebi.PolynomialParameterPath.parameterPath_tendsto
365 #print axioms Komorebi.PolynomialParameterPath.parameterPath_zero
366 #print axioms Komorebi.PolynomialParameterSystem.augmented
367 #print axioms Komorebi.PolynomialParameterSystem.augmented_free
368 #print axioms Komorebi.PolynomialParameterSystem.augmented_jacobian_surjective
369 #print axioms Komorebi.PolynomialParameterSystem.augmented_solved
370 #print axioms Komorebi.PolynomialParameterSystem.continuous_freePart
371 #print axioms Komorebi.PolynomialParameterSystem.continuous_join
372 #print axioms Komorebi.PolynomialParameterSystem.continuous_solvedPart
373 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_augmented
374 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_join_zero
375 #print axioms Komorebi.PolynomialParameterSystem.evalSystem_augmented
376 #print axioms Komorebi.PolynomialParameterSystem.freePart
377 #print axioms Komorebi.PolynomialParameterSystem.freePart_join
378 #print axioms Komorebi.PolynomialParameterSystem.join
379 #print axioms Komorebi.PolynomialParameterSystem.join_free
380 #print axioms Komorebi.PolynomialParameterSystem.join_parts
381 #print axioms Komorebi.PolynomialParameterSystem.join_solved
382 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented
383 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented_iff
384 #print axioms Komorebi.PolynomialParameterSystem.solvedJacobian
385 #print axioms Komorebi.PolynomialParameterSystem.solvedPart
386 #print axioms Komorebi.PolynomialParameterSystem.solvedPart_join
387 #print axioms Komorebi.PolynomialParameterTowerContracts.actual_integer_path_tower
388 #print axioms Komorebi.PolynomialParameterTowerContracts.actual_square_parameter_uniqueness
389 #print axioms Komorebi.PolynomialParameterTowerContracts.arbitrary_padic_parameter_path
390 #print axioms Komorebi.PolynomialParameterTowerContracts.arbitrary_padic_target_tower
391 #print axioms Komorebi.PolynomialParameterTowerContracts.supplied_path_actual_endpoint
392 #print axioms Komorebi.PolynomialParameterTowerControls.firstSolved
393 #print axioms Komorebi.PolynomialParameterTowerControls.firstSolved_surjective
394 #print axioms Komorebi.PolynomialParameterTowerControls.rectangular_same_parameter_nonunique
395 #print axioms Komorebi.PolynomialPrescribedContract.ActualResidues
396 #print axioms Komorebi.PolynomialPrescribedContract.actualResidueEquiv
397 #print axioms Komorebi.PolynomialPrescribedContract.actualSolvedMap
398 #print axioms Komorebi.PolynomialPrescribedContract.actual_lower_root_obstruction
399 #print axioms Komorebi.PolynomialPrescribedContract.actual_lower_root_prime_count
400 #print axioms Komorebi.PolynomialPrescribedControls.digit_one_empty
401 #print axioms Komorebi.PolynomialPrescribedControls.digit_one_for_three_empty
402 #print axioms Komorebi.PolynomialPrescribedControls.digit_two_for_three_exists
403 #print axioms Komorebi.PolynomialPrescribedControls.full_jacobian_surjective
404 #print axioms Komorebi.PolynomialPrescribedControls.parameterOnly
405 #print axioms Komorebi.PolynomialPrescribedControls.parameterPlusThree
406 #print axioms Komorebi.PolynomialPrescribedControls.prescribed_one_for_three_no_actual_lift
407 #print axioms Komorebi.PolynomialPrescribedControls.prescribed_one_no_actual_lift
408 #print axioms Komorebi.PolynomialPrescribedControls.prescribed_two_for_three_actual_lift
409 #print axioms Komorebi.PolynomialPrescribedControls.prescribed_zero_actual_card
410 #print axioms Komorebi.PolynomialPrescribedControls.solved_jacobian_zero
411 #print axioms Komorebi.PolynomialPrescribedControls.three_residual
412 #print axioms Komorebi.PolynomialPrescribedControls.zeroDigitEquiv
413 #print axioms Komorebi.PolynomialPrescribedControls.zero_digit_card
414 #print axioms Komorebi.PolynomialPrescribedControls.zero_residual
415 #print axioms Komorebi.PolynomialPrescribedCounts.digitAddTorsor
416 #print axioms Komorebi.PolynomialPrescribedCounts.digit_card
417 #print axioms Komorebi.PolynomialPrescribedCounts.liftAddTorsor
418 #print axioms Komorebi.PolynomialPrescribedCounts.liftEquivKernel
419 #print axioms Komorebi.PolynomialPrescribedCounts.lift_card
420 #print axioms Komorebi.PolynomialPrescribedCounts.lift_card_eq_kernel
421 #print axioms Komorebi.PolynomialPrescribedCounts.obstruction_card
422 #print axioms Komorebi.PolynomialPrescribedCounts.obstruction_finrank
423 #print axioms Komorebi.PolynomialPrescribedIntegerTower.exists_prescribed_tower
424 #print axioms Komorebi.PolynomialPrescribedIntegerTower.exists_prescribed_tower_strong
425 #print axioms Komorebi.PolynomialPrescribedIntegerTower.tower_solvedJacobian_eq
426 #print axioms Komorebi.PolynomialPrescribedLifts.PrescribedLifts
427 #print axioms Komorebi.PolynomialPrescribedLifts.freePart_digitResidue
428 #print axioms Komorebi.PolynomialPrescribedLifts.prescribedDigitEquivLifts
429 #print axioms Komorebi.PolynomialPrescribedLifts.prescribedDigitEquivLifts_apply
430 #print axioms Komorebi.PolynomialPrescribedLifts.prescribedDigitEquivRestricted
431 #print axioms Komorebi.PolynomialPrescribedLifts.restrictedDigitEquivLifts
432 #print axioms Komorebi.PolynomialPrescribedObstruction.finite_prescribed_lift_count
433 #print axioms Komorebi.PolynomialPrescribedObstruction.finite_prescribed_obstruction
434 #print axioms Komorebi.PolynomialPrescribedObstruction.prescribed_lift_iff_obstruction_zero
435 #print axioms Komorebi.PolynomialPrescribedObstruction.prescribed_obstruction_finite
436 #print axioms Komorebi.PolynomialPrescribedObstruction.prescribed_residue_exists_iff
437 #print axioms Komorebi.PolynomialPrescribedPadicTower.exists_prescribed_padic_root
438 #print axioms Komorebi.PolynomialPrescribedPadicTower.exists_prescribed_padic_root_with_tower
439 #print axioms Komorebi.PolynomialPrescribedPadicTower.exists_root_with_prescribed_path
440 #print axioms Komorebi.PolynomialPrescribedPadicTower.exists_unique_prescribed_padic_root
441 #print axioms Komorebi.PolynomialPrescribedStep.obstruction_zero
442 #print axioms Komorebi.PolynomialPrescribedStep.one_step_lift
443 #print axioms Komorebi.PolynomialPrescribedStep.prescribed_lift_card
444 #print axioms Komorebi.PolynomialPrescribedStep.solvedJacobian_eq
445 #print axioms Komorebi.PolynomialPrescribedStep.solvedJacobian_shift_eq
446 #print axioms Komorebi.PolynomialPrescribedStep.solved_dimension
447 #print axioms Komorebi.PolynomialPrescribedStep.solved_rank
448 #print axioms Komorebi.PolynomialPrescribedSystem.PrescribedDigits
449 #print axioms Komorebi.PolynomialPrescribedSystem.PrescribedObstruction
450 #print axioms Komorebi.PolynomialPrescribedSystem.digitJacobian_join
451 #print axioms Komorebi.PolynomialPrescribedSystem.obstruction
452 #print axioms Komorebi.PolynomialPrescribedSystem.parameterJacobian
453 #print axioms Komorebi.PolynomialPrescribedSystem.parameterResidual
454 #print axioms Komorebi.PolynomialPrescribedSystem.prescribed_digits_finite
455 #print axioms Komorebi.PolynomialPrescribedSystem.prescribed_digits_nonempty_iff
456 #print axioms Komorebi.PolynomialPrescribedSystem.prescribed_equation_iff
457 #print axioms Komorebi.PolynomialPrescribedSystem.solvedJacobian
458 #print axioms Komorebi.PolynomialPrescribedTowerLimit.prescribed_tower_limit
459 #print axioms Komorebi.PolynomialPrescribedTowerUnique.prescribed_root_eq_chartPoint
460 #print axioms Komorebi.PolynomialPrescribedTowerUnique.prescribed_root_unique
461 #print axioms Komorebi.PolynomialPrescribedTowerUnique.prescribed_tower_endpoints_unique
462 #print axioms Komorebi.PolynomialPrescribedTowerUnique.solvedJacobian_square
463 #print axioms Komorebi.PolynomialRegularityContracts.actual_integral_analytic_root_graph
464 #print axioms Komorebi.PolynomialRegularityContracts.actual_padic_analytic_root_graph
465 #print axioms Komorebi.PolynomialRegularityContracts.actual_polynomial_evaluation
466 #print axioms Komorebi.PolynomialRegularityContracts.actual_selection_analytic_on_open
467 #print axioms Komorebi.PolynomialRegularityContracts.actual_selection_germ
468 #print axioms Komorebi.PolynomialRegularityControls.linearSystem
469 #print axioms Komorebi.PolynomialRegularityControls.linear_analytic
470 #print axioms Komorebi.PolynomialRegularityControls.linear_derivative_not_positive
471 #print axioms Komorebi.PolynomialRegularityControls.linear_parameterJacobian
472 #print axioms Komorebi.PolynomialRegularityControls.linear_root_graph
473 #print axioms Komorebi.PolynomialRegularityControls.linear_solvedJacobian
474 #print axioms Komorebi.PolynomialRegularityControls.linear_strict_derivative
475 #print axioms Komorebi.PolynomialRegularityControls.quadraticSystem
476 #print axioms Komorebi.PolynomialRegularityControls.quadratic_analytic_branch
477 #print axioms Komorebi.PolynomialRegularityControls.quadratic_parameterJacobian
478 #print axioms Komorebi.PolynomialRegularityControls.quadratic_root
479 #print axioms Komorebi.PolynomialRegularityControls.quadratic_solvedJacobian
480 #print axioms Komorebi.PolynomialRegularityIntegral.eval_pderiv_rationalSystem
481 #print axioms Komorebi.PolynomialRegularityIntegral.eval_rationalSystem
482 #print axioms Komorebi.PolynomialRegularityIntegral.exists_analytic_integral_implicit
483 #print axioms Komorebi.PolynomialRegularityIntegral.parameterJacobian_rationalSystem
484 #print axioms Komorebi.PolynomialRegularityIntegral.rationalPoint
485 #print axioms Komorebi.PolynomialRegularityIntegral.rationalPoint_freePart
486 #print axioms Komorebi.PolynomialRegularityIntegral.rationalPoint_join
487 #print axioms Komorebi.PolynomialRegularityIntegral.rationalPoint_solvedPart
488 #print axioms Komorebi.PolynomialRegularityIntegral.rationalSystem
489 #print axioms Komorebi.PolynomialRegularityIntegral.rationalSystem_root
490 #print axioms Komorebi.PolynomialRegularityIntegral.solvedJacobian_rationalSystem
491 #print axioms Komorebi.PolynomialRootMotion.exists_perturbed_root_certificate
492 #print axioms Komorebi.PolynomialRootMotion.exists_root_from_original_preconditioner
493 #print axioms Komorebi.PolynomialRootMotion.exists_root_motion
494 #print axioms Komorebi.PolynomialRootMotion.exists_unique_root_motion
495 #print axioms Komorebi.PolynomialRootMotionContract.original_jacobian_integral_error
496 #print axioms Komorebi.PolynomialRootMotionContract.original_jacobian_rational_motion
497 #print axioms Komorebi.PolynomialRootStability.exists_nearby_perturbed_root
498 #print axioms Komorebi.PolynomialRootStability.exists_root_and_unique_perturbation
499 #print axioms Komorebi.PolynomialRootStability.exists_unique_nearby_perturbed_root
500 #print axioms Komorebi.PolynomialRootStability.integer_congruent_of_common_padic
501 #print axioms Komorebi.PolynomialRootStability.perturbed_roots_congruent
502 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_lower_root_and_unique_perturbation
503 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_rectangular_nearby_root
504 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_square_root_displacement
505 #print axioms Komorebi.PolynomialSmoothCounts.exists_regular_tower
506 #print axioms Komorebi.PolynomialSmoothCounts.smooth_dimension
507 #print axioms Komorebi.PolynomialSmoothCounts.smooth_lift_card
508 #print axioms Komorebi.PolynomialSmoothCounts.smooth_obstruction_card
509 #print axioms Komorebi.PolynomialSmoothCounts.smooth_rank
510 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_eq
511 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_shift_eq
512 #print axioms Komorebi.PolynomialSurjectiveStep.one_step_lift
513 #print axioms Komorebi.PolynomialTaylor.directional
514 #print axioms Komorebi.PolynomialTaylor.directional_C
515 #print axioms Komorebi.PolynomialTaylor.directional_X
516 #print axioms Komorebi.PolynomialTaylor.directional_add
517 #print axioms Komorebi.PolynomialTaylor.directional_mul
518 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
519 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
520 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
521 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
522 #print axioms Komorebi.PolynomialTaylorDisplacement.taylor_remainder_dvd
523 #print axioms Komorebi.PolynomialTaylorRing.eval_dvd_of_dvd
524 #print axioms Komorebi.PolynomialTaylorRing.eval_linearPart
525 #print axioms Komorebi.PolynomialTaylorRing.eval_scaled_bind
526 #print axioms Komorebi.PolynomialTaylorRing.eval_zero_linearPart
527 #print axioms Komorebi.PolynomialTaylorRing.exists_eval_scaled_remainder
528 #print axioms Komorebi.PolynomialTaylorRing.exists_scaled_remainder
529 #print axioms Komorebi.PolynomialTaylorRing.linearPart
530 #print axioms Komorebi.PolynomialTaylorRing.linearPart_C
531 #print axioms Komorebi.PolynomialTaylorRing.linearPart_X
532 #print axioms Komorebi.PolynomialTaylorRing.linearPart_add
533 #print axioms Komorebi.PolynomialTaylorRing.linearPart_mul
534 #print axioms Komorebi.PolynomialTowerControls.linearMinusTwo
535 #print axioms Komorebi.PolynomialTowerControls.linear_shift_no_extra_precision
536 #print axioms Komorebi.PolynomialTowerControls.linear_shift_nonsingular_lower_root
537 #print axioms Komorebi.PolynomialTowerControls.projectionSystem
538 #print axioms Komorebi.PolynomialTowerControls.projection_jacobian_surjective
539 #print axioms Komorebi.PolynomialTowerControls.projection_two_padic_roots
540 #print axioms Komorebi.PolynomialTowerControls.squareMinusFive
541 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_lower_steps
542 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_mod_eight
543 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_tower
544 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.actual_polynomial_contraction
545 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.exact_inverse_denominator_certificate
546 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.uniform_polynomial_taylor
547 #print axioms Komorebi.PolynomialWeightedControls.boundary_exact_residual_depth
548 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_mod_eight
549 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_padic_root
550 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_root
551 #print axioms Komorebi.PolynomialWeightedControls.boundary_residual_derivative
552 #print axioms Komorebi.PolynomialWeightedControls.boundary_scaled_inverse
553 #print axioms Komorebi.PolynomialWeightedControls.linear_displacement_sharp
554 #print axioms Komorebi.PolynomialWeightedControls.linear_perturbation_root
555 #print axioms Komorebi.PolynomialWeightedControls.prime_power_exact_depth
556 #print axioms Komorebi.PolynomialWeightedControls.squarePlusThree
557 #print axioms Komorebi.PolynomialWeightedControls.weightedLinear
558 #print axioms Komorebi.PolynomialWeightedInverse.bounded_inverse_iff_certificate
559 #print axioms Komorebi.PolynomialWeightedInverse.certificate_of_integral_inverse
560 #print axioms Komorebi.PolynomialWeightedInverse.eval_precondition
561 #print axioms Komorebi.PolynomialWeightedInverse.integral_inverse_iff_certificate
562 #print axioms Komorebi.PolynomialWeightedInverse.integral_inverse_of_certificate
563 #print axioms Komorebi.PolynomialWeightedInverse.jacobian
564 #print axioms Komorebi.PolynomialWeightedInverse.jacobian_precondition
565 #print axioms Komorebi.PolynomialWeightedInverse.mulVec_injective_of_scalar_certificate
566 #print axioms Komorebi.PolynomialWeightedInverse.mulVec_preserves_dvd
567 #print axioms Komorebi.PolynomialWeightedInverse.padic_mulVec_injective
568 #print axioms Komorebi.PolynomialWeightedInverse.precondition
569 #print axioms Komorebi.PolynomialWeightedInverse.precondition_root_iff
570 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix
571 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_injective
572 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_isUnit_of_certificate
573 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_mul
574 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_scalar
575 #print axioms Komorebi.PolynomialWeightedLift.exists_root_of_normalization
576 #print axioms Komorebi.PolynomialWeightedLift.exists_unique_weighted_root
577 #print axioms Komorebi.PolynomialWeightedLift.exists_weighted_root
578 #print axioms Komorebi.PolynomialWeightedLift.exists_weighted_root_certificate
579 #print axioms Komorebi.PolynomialWeightedLift.shiftedPoint
580 #print axioms Komorebi.PolynomialWeightedLiftContract.actual_jacobian_bounded_inverse
581 #print axioms Komorebi.PolynomialWeightedLiftContract.actual_jacobian_integral_certificate
582 #print axioms Komorebi.PolynomialWeightedNormalization.exists_normalization
583 #print axioms Komorebi.PolynomialWeightedNormalization.precondition_directional
584 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
585 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
586 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
587 #print axioms Komorebi.ResidueLiftDigits.digitResidue
588 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
589 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
590 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
591 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
592 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
593 #print axioms Komorebi.ResidueLiftDigits.shift_cast_eq_iff

Back to source controls