PolynomialParameterTowerAxiomAudit.lean

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

Back to source controls