PolynomialWeightedAxiomAudit.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 PolynomialObstruction
13 public import PolynomialWeightedNormalization
14 public import PolynomialDigitBridge
15 public import PolynomialWeightedLift
16 public import PolynomialLiftCounts
17 public import PolynomialSurjectiveStep
18 public import PolynomialIntegerTower
19 public import PolynomialSmoothCounts
20 public import PolynomialTowerControls
21 public import PolynomialPadicLift
22 public import PolynomialCoefficientPerturbation
23 public import PolynomialPadicUnique
24 public import PolynomialParameterSystem
25 public import PolynomialCoordinateReorder
26 public import PolynomialInverseCongruence
27 public import PolynomialLocalSurjective
28 public import PolynomialRootStability
29 public import PolynomialLocalInverse
30 public import PolynomialParameterChart
31 public import PolynomialGeneralChart
32 public import PolynomialDeformationControls
33 public import PolynomialParameterControls
34 public import PolynomialWeightedControls
35 public import PolynomialCoefficientPerturbationContract
36 public import PolynomialGeneralChartContract
37 public import PolynomialHomeomorphContract
38 public import PolynomialLocalMapContract
39 public import PolynomialPadicUniqueContract
40 public import PolynomialRootStabilityContract
41 public import PolynomialWeightedAuxiliaryContract
42 public import PolynomialWeightedLiftContract
43 @[expose] public section
44 #print axioms Komorebi.FiniteFiberCounts.Fiber
45 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
46 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
47 #print axioms Komorebi.FiniteFiberCounts.difference
48 #print axioms Komorebi.FiniteFiberCounts.difference_translate
49 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
50 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
51 #print axioms Komorebi.FiniteFiberCounts.fiber_card
52 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
53 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
54 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
55 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
56 #print axioms Komorebi.FiniteFiberCounts.kernel_card
57 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
58 #print axioms Komorebi.FiniteFiberCounts.rank
59 #print axioms Komorebi.FiniteFiberCounts.translate
60 #print axioms Komorebi.FiniteFiberCounts.translate_add
61 #print axioms Komorebi.FiniteFiberCounts.translate_difference
62 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
63 #print axioms Komorebi.FiniteFiberCounts.translate_zero
64 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
65 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
66 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
67 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
68 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
69 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
70 #print axioms Komorebi.NativeAffine.Obstruction
71 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
72 #print axioms Komorebi.NativeAffine.affine_residual_transport
73 #print axioms Komorebi.NativeAffine.digitMap
74 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
75 #print axioms Komorebi.NativeAffine.obstruction
76 #print axioms Komorebi.NativeAffine.obstruction_finite
77 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
78 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
79 #print axioms Komorebi.NativeAffine.reduction
80 #print axioms Komorebi.NativeAffine.reduction_zero_iff
81 #print axioms Komorebi.NativeAffine.residual_exists
82 #print axioms Komorebi.NativeAffine.same_residue_iff
83 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
84 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
85 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit
86 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
87 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
88 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
89 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_eq
90 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_point_eq
91 #print axioms Komorebi.PolynomialCoefficientPerturbation.evalSystem_perturb
92 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_perturb
93 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_power_perturb
94 #print axioms Komorebi.PolynomialCoefficientPerturbation.lower_root_perturb
95 #print axioms Komorebi.PolynomialCoefficientPerturbation.padicEval_perturb
96 #print axioms Komorebi.PolynomialCoefficientPerturbation.pderiv_perturb
97 #print axioms Komorebi.PolynomialCoefficientPerturbation.perturb
98 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_perturbed_jacobian
99 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_power_perturbation_root
100 #print axioms Komorebi.PolynomialCoordinateReorder.continuous_reorderPoint
101 #print axioms Komorebi.PolynomialCoordinateReorder.digitJacobian_single
102 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder
103 #print axioms Komorebi.PolynomialCoordinateReorder.evalSystem_reorder_at
104 #print axioms Komorebi.PolynomialCoordinateReorder.exists_reorder_solvedJacobian_surjective
105 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder
106 #print axioms Komorebi.PolynomialCoordinateReorder.padicEval_reorder_at
107 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_eval_reorder
108 #print axioms Komorebi.PolynomialCoordinateReorder.pderiv_reorder
109 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint
110 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse
111 #print axioms Komorebi.PolynomialCoordinateReorder.reorderPoint_inverse'
112 #print axioms Komorebi.PolynomialCoordinateReorder.reorderSystem
113 #print axioms Komorebi.PolynomialCoordinateReorder.solvedJacobian_reorder_apply
114 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_coefficient_perturbation
115 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_no_extra_padic_precision
116 #print axioms Komorebi.PolynomialDeformationControls.squareMinusOne
117 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_jacobian_bijective
118 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_not_global_unique
119 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_two_padic_roots
120 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
121 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
122 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
123 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
124 #print axioms Komorebi.PolynomialDigitBridge.integerLift
125 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
126 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
127 #print axioms Komorebi.PolynomialGeneralChart.exists_parameter_homeomorph
128 #print axioms Komorebi.PolynomialGeneralChart.reorderRootHomeomorph
129 #print axioms Komorebi.PolynomialGeneralChartContract.full_rectangular_chart
130 #print axioms Komorebi.PolynomialHomeomorphContract.square_homeomorphism
131 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower
132 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong
133 #print axioms Komorebi.PolynomialIntegerTower.tower_digitJacobian_eq
134 #print axioms Komorebi.PolynomialIntegerTower.tower_initial_congruent
135 #print axioms Komorebi.PolynomialIntegerTower.tower_pairwise_congruent
136 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence
137 #print axioms Komorebi.PolynomialInverseCongruence.integer_inverse_congruence_step
138 #print axioms Komorebi.PolynomialInverseCongruence.padicEval_congruent
139 #print axioms Komorebi.PolynomialInverseCongruence.padic_congruence_iff
140 #print axioms Komorebi.PolynomialInverseCongruence.padic_inverse_congruence
141 #print axioms Komorebi.PolynomialInverseCongruence.padic_map_injective
142 #print axioms Komorebi.PolynomialLiftCounts.ActualLifts
143 #print axioms Komorebi.PolynomialLiftCounts.digitAddTorsor
144 #print axioms Komorebi.PolynomialLiftCounts.digitEquivLifts
145 #print axioms Komorebi.PolynomialLiftCounts.digit_residue_solution_iff
146 #print axioms Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count
147 #print axioms Komorebi.PolynomialLiftCounts.liftEquivKernel
148 #print axioms Komorebi.PolynomialLiftCounts.lift_card
149 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv
150 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv_class
151 #print axioms Komorebi.PolynomialLiftCounts.obstruction_card
152 #print axioms Komorebi.PolynomialLocalInverse.ballMap
153 #print axioms Komorebi.PolynomialLocalInverse.ballMap_bijective
154 #print axioms Komorebi.PolynomialLocalInverse.continuous_ballMap
155 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph
156 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_apply
157 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_congruent
158 #print axioms Komorebi.PolynomialLocalInverse.localHomeomorph_symm_eval
159 #print axioms Komorebi.PolynomialLocalMapContract.all_depths_reflected
160 #print axioms Komorebi.PolynomialLocalMapContract.arbitrary_padic_target
161 #print axioms Komorebi.PolynomialLocalSurjective.digitJacobian_sub_C
162 #print axioms Komorebi.PolynomialLocalSurjective.exists_integer_target_preimage
163 #print axioms Komorebi.PolynomialLocalSurjective.exists_padic_preimage
164 #print axioms Komorebi.PolynomialLocalSurjective.isClosed_residueBall
165 #print axioms Komorebi.PolynomialLocalSurjective.isCompact_residueBall
166 #print axioms Komorebi.PolynomialLocalSurjective.residueBall
167 #print axioms Komorebi.PolynomialLocalSurjective.truncInt_tendsto
168 #print axioms Komorebi.PolynomialMinorSelection.exists_permuted_columns
169 #print axioms Komorebi.PolynomialMinorSelection.exists_prime_permuted_columns
170 #print axioms Komorebi.PolynomialMinorSelection.exists_selected_columns
171 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
172 #print axioms Komorebi.PolynomialObstruction.evalSystem
173 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
174 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
175 #print axioms Komorebi.PolynomialObstruction.jacobian
176 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
177 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
178 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
179 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
180 #print axioms Komorebi.PolynomialObstruction.residual_exists
181 #print axioms Komorebi.PolynomialObstruction.residual_unique
182 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
183 #print axioms Komorebi.PolynomialPadicContraction.contracting_contractionMap
184 #print axioms Komorebi.PolynomialPadicContraction.contractionMap
185 #print axioms Komorebi.PolynomialPadicContraction.evalSystem
186 #print axioms Komorebi.PolynomialPadicContraction.eval_dist_le
187 #print axioms Komorebi.PolynomialPadicContraction.eval_dvd_of_dvd
188 #print axioms Komorebi.PolynomialPadicContraction.exists_unique_fixedPoint
189 #print axioms Komorebi.PolynomialPadicContraction.exists_unique_fixedPoint_divisible
190 #print axioms Komorebi.PolynomialPadicContraction.fixedPoint_divisible
191 #print axioms Komorebi.PolynomialPadicContraction.lipschitz_evalSystem
192 #print axioms Komorebi.PolynomialPadicLift.continuous_padicEval
193 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root
194 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root_with_tower
195 #print axioms Komorebi.PolynomialPadicLift.padicEval
196 #print axioms Komorebi.PolynomialPadicLift.padicEval_intCast
197 #print axioms Komorebi.PolynomialPadicLift.polynomial_tower_limit_root
198 #print axioms Komorebi.PolynomialPadicUnique.exists_unique_padic_root
199 #print axioms Komorebi.PolynomialPadicUnique.int_pow_dvd_iff
200 #print axioms Komorebi.PolynomialPadicUnique.padic_root_unique
201 #print axioms Komorebi.PolynomialPadicUnique.rootResidueLift
202 #print axioms Komorebi.PolynomialPadicUnique.root_next_residue_eq
203 #print axioms Komorebi.PolynomialPadicUnique.toZModPow_eq_iff_dvd_sub
204 #print axioms Komorebi.PolynomialPadicUnique.truncInt
205 #print axioms Komorebi.PolynomialPadicUnique.truncInt_eval_residue
206 #print axioms Komorebi.PolynomialPadicUnique.truncInt_precision
207 #print axioms Komorebi.PolynomialPadicUnique.truncInt_root
208 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_arbitrary_root_uniqueness
209 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_unique_padic_root
210 #print axioms Komorebi.PolynomialParameterChart.chartGraph_iff
211 #print axioms Komorebi.PolynomialParameterChart.chartPhi
212 #print axioms Komorebi.PolynomialParameterChart.chartPoint
213 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent
214 #print axioms Komorebi.PolynomialParameterChart.chartPoint_congruent_iff
215 #print axioms Komorebi.PolynomialParameterChart.chartPoint_free
216 #print axioms Komorebi.PolynomialParameterChart.chartPoint_graph
217 #print axioms Komorebi.PolynomialParameterChart.chartPoint_root
218 #print axioms Komorebi.PolynomialParameterChart.chartPoint_spec
219 #print axioms Komorebi.PolynomialParameterChart.chartPoint_unique
220 #print axioms Komorebi.PolynomialParameterChart.chartTarget
221 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPhi
222 #print axioms Komorebi.PolynomialParameterChart.continuous_chartPoint
223 #print axioms Komorebi.PolynomialParameterChart.continuous_chartTarget
224 #print axioms Komorebi.PolynomialParameterChart.parameterHomeomorph
225 #print axioms Komorebi.PolynomialParameterControls.full_jacobian_surjective
226 #print axioms Komorebi.PolynomialParameterControls.no_root_at_parameter_two
227 #print axioms Komorebi.PolynomialParameterControls.parameter_two_near_origin
228 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_not_surjective
229 #print axioms Komorebi.PolynomialParameterControls.solved_jacobian_zero
230 #print axioms Komorebi.PolynomialParameterControls.squareMinusParameter
231 #print axioms Komorebi.PolynomialParameterSystem.augmented
232 #print axioms Komorebi.PolynomialParameterSystem.augmented_free
233 #print axioms Komorebi.PolynomialParameterSystem.augmented_jacobian_surjective
234 #print axioms Komorebi.PolynomialParameterSystem.augmented_solved
235 #print axioms Komorebi.PolynomialParameterSystem.continuous_freePart
236 #print axioms Komorebi.PolynomialParameterSystem.continuous_join
237 #print axioms Komorebi.PolynomialParameterSystem.continuous_solvedPart
238 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_augmented
239 #print axioms Komorebi.PolynomialParameterSystem.digitJacobian_join_zero
240 #print axioms Komorebi.PolynomialParameterSystem.evalSystem_augmented
241 #print axioms Komorebi.PolynomialParameterSystem.freePart
242 #print axioms Komorebi.PolynomialParameterSystem.freePart_join
243 #print axioms Komorebi.PolynomialParameterSystem.join
244 #print axioms Komorebi.PolynomialParameterSystem.join_free
245 #print axioms Komorebi.PolynomialParameterSystem.join_parts
246 #print axioms Komorebi.PolynomialParameterSystem.join_solved
247 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented
248 #print axioms Komorebi.PolynomialParameterSystem.padicEval_augmented_iff
249 #print axioms Komorebi.PolynomialParameterSystem.solvedJacobian
250 #print axioms Komorebi.PolynomialParameterSystem.solvedPart
251 #print axioms Komorebi.PolynomialParameterSystem.solvedPart_join
252 #print axioms Komorebi.PolynomialRootStability.exists_nearby_perturbed_root
253 #print axioms Komorebi.PolynomialRootStability.exists_root_and_unique_perturbation
254 #print axioms Komorebi.PolynomialRootStability.exists_unique_nearby_perturbed_root
255 #print axioms Komorebi.PolynomialRootStability.integer_congruent_of_common_padic
256 #print axioms Komorebi.PolynomialRootStability.perturbed_roots_congruent
257 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_lower_root_and_unique_perturbation
258 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_rectangular_nearby_root
259 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_square_root_displacement
260 #print axioms Komorebi.PolynomialSmoothCounts.exists_regular_tower
261 #print axioms Komorebi.PolynomialSmoothCounts.smooth_dimension
262 #print axioms Komorebi.PolynomialSmoothCounts.smooth_lift_card
263 #print axioms Komorebi.PolynomialSmoothCounts.smooth_obstruction_card
264 #print axioms Komorebi.PolynomialSmoothCounts.smooth_rank
265 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_eq
266 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_shift_eq
267 #print axioms Komorebi.PolynomialSurjectiveStep.one_step_lift
268 #print axioms Komorebi.PolynomialTaylor.directional
269 #print axioms Komorebi.PolynomialTaylor.directional_C
270 #print axioms Komorebi.PolynomialTaylor.directional_X
271 #print axioms Komorebi.PolynomialTaylor.directional_add
272 #print axioms Komorebi.PolynomialTaylor.directional_mul
273 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
274 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
275 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
276 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
277 #print axioms Komorebi.PolynomialTaylorRing.eval_dvd_of_dvd
278 #print axioms Komorebi.PolynomialTaylorRing.eval_linearPart
279 #print axioms Komorebi.PolynomialTaylorRing.eval_scaled_bind
280 #print axioms Komorebi.PolynomialTaylorRing.eval_zero_linearPart
281 #print axioms Komorebi.PolynomialTaylorRing.exists_eval_scaled_remainder
282 #print axioms Komorebi.PolynomialTaylorRing.exists_scaled_remainder
283 #print axioms Komorebi.PolynomialTaylorRing.linearPart
284 #print axioms Komorebi.PolynomialTaylorRing.linearPart_C
285 #print axioms Komorebi.PolynomialTaylorRing.linearPart_X
286 #print axioms Komorebi.PolynomialTaylorRing.linearPart_add
287 #print axioms Komorebi.PolynomialTaylorRing.linearPart_mul
288 #print axioms Komorebi.PolynomialTowerControls.linearMinusTwo
289 #print axioms Komorebi.PolynomialTowerControls.linear_shift_no_extra_precision
290 #print axioms Komorebi.PolynomialTowerControls.linear_shift_nonsingular_lower_root
291 #print axioms Komorebi.PolynomialTowerControls.projectionSystem
292 #print axioms Komorebi.PolynomialTowerControls.projection_jacobian_surjective
293 #print axioms Komorebi.PolynomialTowerControls.projection_two_padic_roots
294 #print axioms Komorebi.PolynomialTowerControls.squareMinusFive
295 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_lower_steps
296 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_mod_eight
297 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_tower
298 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.actual_polynomial_contraction
299 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.exact_inverse_denominator_certificate
300 #print axioms Komorebi.PolynomialWeightedAuxiliaryContract.uniform_polynomial_taylor
301 #print axioms Komorebi.PolynomialWeightedControls.boundary_exact_residual_depth
302 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_mod_eight
303 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_padic_root
304 #print axioms Komorebi.PolynomialWeightedControls.boundary_no_root
305 #print axioms Komorebi.PolynomialWeightedControls.boundary_residual_derivative
306 #print axioms Komorebi.PolynomialWeightedControls.boundary_scaled_inverse
307 #print axioms Komorebi.PolynomialWeightedControls.linear_displacement_sharp
308 #print axioms Komorebi.PolynomialWeightedControls.linear_perturbation_root
309 #print axioms Komorebi.PolynomialWeightedControls.prime_power_exact_depth
310 #print axioms Komorebi.PolynomialWeightedControls.squarePlusThree
311 #print axioms Komorebi.PolynomialWeightedControls.weightedLinear
312 #print axioms Komorebi.PolynomialWeightedInverse.bounded_inverse_iff_certificate
313 #print axioms Komorebi.PolynomialWeightedInverse.certificate_of_integral_inverse
314 #print axioms Komorebi.PolynomialWeightedInverse.eval_precondition
315 #print axioms Komorebi.PolynomialWeightedInverse.integral_inverse_iff_certificate
316 #print axioms Komorebi.PolynomialWeightedInverse.integral_inverse_of_certificate
317 #print axioms Komorebi.PolynomialWeightedInverse.jacobian
318 #print axioms Komorebi.PolynomialWeightedInverse.jacobian_precondition
319 #print axioms Komorebi.PolynomialWeightedInverse.mulVec_injective_of_scalar_certificate
320 #print axioms Komorebi.PolynomialWeightedInverse.mulVec_preserves_dvd
321 #print axioms Komorebi.PolynomialWeightedInverse.padic_mulVec_injective
322 #print axioms Komorebi.PolynomialWeightedInverse.precondition
323 #print axioms Komorebi.PolynomialWeightedInverse.precondition_root_iff
324 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix
325 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_injective
326 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_isUnit_of_certificate
327 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_mul
328 #print axioms Komorebi.PolynomialWeightedInverse.rationalMatrix_scalar
329 #print axioms Komorebi.PolynomialWeightedLift.exists_root_of_normalization
330 #print axioms Komorebi.PolynomialWeightedLift.exists_unique_weighted_root
331 #print axioms Komorebi.PolynomialWeightedLift.exists_weighted_root
332 #print axioms Komorebi.PolynomialWeightedLift.exists_weighted_root_certificate
333 #print axioms Komorebi.PolynomialWeightedLift.shiftedPoint
334 #print axioms Komorebi.PolynomialWeightedLiftContract.actual_jacobian_bounded_inverse
335 #print axioms Komorebi.PolynomialWeightedLiftContract.actual_jacobian_integral_certificate
336 #print axioms Komorebi.PolynomialWeightedNormalization.exists_normalization
337 #print axioms Komorebi.PolynomialWeightedNormalization.precondition_directional
338 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
339 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
340 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
341 #print axioms Komorebi.ResidueLiftDigits.digitResidue
342 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
343 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
344 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
345 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
346 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
347 #print axioms Komorebi.ResidueLiftDigits.shift_cast_eq_iff

Back to source controls