promachina/iut-lean
failedIndexed33821theorem-like declarations
Sorries left0%0 markers in 0 declarations
Blueprint19 nodes to go
61 of 80 proved3 ready16 blocked
| Theorem | Status | Owner | Module | Last run |
|---|---|---|---|---|
| _abel_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1 | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| _abel_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_1 | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| _abel_1_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_1 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_2 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_1_2 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| _abel_2 | Checked | unowned | Iut/Foundations/SourceModelFrobenioid.lean | |
| abs_injective_on_parameterSet | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| absLabelAverageCoefficient_gt_one | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelFromProcession_core | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelFromProcession_injective | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelFromProcession_injective | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelFromProcession_surjective | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelFromProcession_surjective | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcession_card_eq_half_plus_one | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelProcessionCard_eq_halfPlusOne | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcession_core_maps_to_zero | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionEquivFullLabel_apply | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionEquivFullLabel_apply | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelProcession_thetaExponent_eq_square | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionTop_eq_half_minus_one | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelProcessionTop_eq_halfMinusOne | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionTop_ge_two | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelProcessionTop_ge_two | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionTop_pos | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabelProcessionTop_pos | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabelProcession_value_le_half | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absLabel_thetaExponent_matches_halfRange_j2 | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLabel_thetaPilot_degree_matches_halfRange_j2 | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| absLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| absLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| absLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| absNonzeroIndexNatCast_ne_neg | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absNonzeroIndexNatCast_ne_zero | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absNonzeroIndexNatCast_val | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absNonzeroLabelAverageCoefficient_gt_fullLabelAverageCoefficient | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| absoluteGalois_def | Checked | unowned | Iut/Foundations/SourceInitialThetaData.lean | |
| absoluteLabel_choiceAt | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absolute_label_choice_audit | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| absoluteLabel_eq_iff | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLabel_neg | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLabel_nonzero | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLabelProcessionAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLabelProcessionChoiceAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLabel_zero | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| absoluteLogQ_degree_window | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| absoluteLogQ_degree_window | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| absoluteLogQ_eq | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| absoluteLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| absoluteLogQ_pos | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| absThetaPilotDegree_distinguishes_one_two_of_q_ne_zero | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| absThetaPilotDegree_one_two_equal_iff_q_zero | Checked | unowned | Iut/Stage1/IUTStage1Experiments/Diagnostics.lean | |
| acted_factor_eq | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| acted_factor_eq | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| acted_product_eq_sum | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| actedProductLogVolume_eq_original_plus_unitCopies | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| acted_tensor_packet_eq_sum | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| actedTensorPacketLogVolume_eq_original_plus_generators | Checked | unowned | Iut/Stage1/IUTStage1Gaussian.lean | |
| actIncidentBranch_bijective | Checked | unowned | Iut/Foundations/SourceSemiGraphAction.lean | |
| actIncidentBranch_injective | Checked | unowned | Iut/Foundations/SourceSemiGraphAction.lean | |
| actIncidentBranch_surjective | Checked | unowned | Iut/Foundations/SourceSemiGraphAction.lean | |
| act_inv | Checked | unowned | Iut/Foundations/ContinuousH1.lean | |
| action_absolute_label_eq | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_absolute_label_eq | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_add | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_apply | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| actionAudit | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_compatible | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_compatible | Checked | unowned | Iut/Foundations/SourceThetaHodgeTheater.lean | |
| action_compatible | Checked | unowned | Iut/Foundations/SourceThetaHodgeTheater.lean | |
| action_connected | Checked | unowned | Iut/Foundations/SourceTemperoidQuotient.lean | |
| actionCount_eq_fiberCardinality | Checked | unowned | Iut/Stage1/IUTStage1HodgeSHE.lean | |
| actionCount_eq_fiberCardinality | Checked | unowned | Iut/Stage1/IUTStage1HodgeSHE.lean | |
| actionCountForKind_archimedean | Checked | unowned | Iut/Stage1/IUTStage1HodgeSHE.lean | |
| actionCountForKind_nonarchimedean | Checked | unowned | Iut/Stage1/IUTStage1HodgeSHE.lean | |
| action_entry_mem | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| action_entry_mem | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| action_entry_mem | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| action_entry_mem | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| action_equalityQuotientMap_eq | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_equalityQuotientMap_eq | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_is_conjugation | Checked | unowned | Iut/Foundations/EtaleThetaCovers.lean | |
| action_isConnected | Checked | unowned | Iut/Foundations/SourceConnectedCoveringQuotient.lean | |
| action_label_cardinality | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_label_cardinality | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_law_audit | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| actionLawAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionLawAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionLawAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionMap_injective | Checked | unowned | Iut/Foundations/SourceThetaEvaluation.lean | |
| action_maps_domain_iff | Checked | unowned | Iut/Foundations/SourceTopologicalPseudoMonoid.lean | |
| action_mul | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_mul | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_mul | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_mul_functor | Checked | unowned | Iut/Foundations/SourceThetaHodgeTheater.lean | |
| action_obj_carrier | Checked | unowned | Iut/Foundations/SourceTemperoidQuotient.lean | |
| action_obj_carrier | Checked | unowned | Iut/Foundations/SourceConnectedCoveringQuotient.lean | |
| action_one | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_one | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_one | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| action_one_functor | Checked | unowned | Iut/Foundations/SourceThetaHodgeTheater.lean | |
| action_partialMul | Checked | unowned | Iut/Foundations/SourceTopologicalPseudoMonoid.lean | |
| action_projects_to_concrete | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| actionRes_preservesFiniteColimits | Checked | unowned | Iut/Foundations/SourceContinuousAnabelioid.lean | |
| actionRes_preservesFiniteLimits | Checked | unowned | Iut/Foundations/SourceContinuousAnabelioid.lean | |
| actionStep_preserves_capsuleCount | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionStep_preserves_capsuleNormalizedLogVolume | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionStep_preserves_capsuleTotalLogVolume | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| actionStep_preserves_directSummandCount | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| action_transition_label_eq | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| action_translateElement_eq | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| action_zero | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| act_mem_target | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| act_mul | Checked | unowned | Iut/Foundations/ContinuousH1.lean | |
| act_mul_group | Checked | unowned | Iut/Foundations/ContinuousH1.lean | |
| act_one | Checked | unowned | Iut/Foundations/ContinuousH1.lean | |
| act_one_group | Checked | unowned | Iut/Foundations/ContinuousH1.lean | |
| actSection_apply | Checked | unowned | Iut/Foundations/SourceSemiGraphAction.lean | |
| addCircleVolume_image_of_injOn | Checked | unowned | Iut/Foundations/SourceTheorem311.lean | |
| add_gluingTranslate | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveFormulaGapAudit | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| additiveHaarAdjustedRawLogVolumeMatchesDifferentPlusConductor | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarArithmeticDegreeCalibrationAuditThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltFinitePlaceLocalGlobalCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltFinitePlaceLocalGlobalCThetaSourceDirect | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltIUTIVCThetaCoupledArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltLocalizedStepXILocalTermCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceConstructorBuiltLocalizedStepXILocalTermCThetaSourceDirect | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofAdditiveHaarConstructedSourceIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofIntrinsicHaarModulusAdditiveHaarConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofIntrinsicHaarModulusAdditiveHaarIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofIntrinsicHaarModulusConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofIntrinsicHaarModulusIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceArithmeticResidual | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceConstructorBuiltFinitePlaceLocalGlobalCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceConstructorBuiltIUTIVCThetaCoupledArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceConstructorBuiltLocalizedStepXILocalTermCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofNormalizedSourceIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleInverseBasePrimeAdditiveHaarConstructedIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleInverseBasePrimeConstructedGaussianHodgeProjectedAdditiveHaarIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleUnitBallHaarCharacterAdditiveHaarConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleUnitBallHaarCharacterAdditiveHaarIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleUnitBallHaarCharacterConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofResidueModuleUnitBallHaarCharacterIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofUnitBallHaarCharacterAdditiveHaarConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofUnitBallHaarCharacterAdditiveHaarIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofUnitBallHaarCharacterStructureSheafNormalizedConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDegreePadicRemainingPayloadAudit_ofUnitBallHaarCharacterStructureSheafNormalizedIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticDivisorFormulaSplitConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarArithmeticResidualPayloadAudit_ofConstructorBuiltFinitePlaceLocalGlobalCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticResidualPayloadAudit_ofConstructorBuiltIUTIVCTheta | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticResidualPayloadAudit_ofConstructorBuiltIUTIVCThetaArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticResidualPayloadAudit_ofConstructorBuiltLocalizedStepXILocalTermCThetaSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarArithmeticResidualPayloadAudit_ofIUTIVCTheta | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarConstructedAPTDatumQuotientEndpointThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedAPTTransportAuditThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedAPTTransportNotForbiddenThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedBoundary | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarConstructedHodgeSHEIPLAPTStructuresThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedIPLCertificateAlignmentThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedIPLChoiceLinkEndpointThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedIPLSHEAPTTransportLawAuditThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedSHEAPTTransportGuardsThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarConstructedSHENoDomainToCodomainTransportThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarEvaluationEndpoint | Checked | unowned | Iut/Stage1/IUTStage1Experiments/AdditiveHaar.lean | |
| additiveHaarEvaluationSourceAudit | Checked | unowned | Iut/Stage1/IUTStage1Experiments/AdditiveHaar.lean | |
| additiveHaarFactor_compactOpenMeasure_eq_one | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveHaarFactor_compactOpenMeasure_ge_one | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveHaarFactor_componentwiseEqual_of_padicFiniteExtensionFactor_componentwiseEqual | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveHaarFactor_componentwiseEqual_of_padicFiniteExtensionFactor_eq | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveHaarFactor_eq_inverseBasePrimeUnitBall | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarFactor_normalizedHaarLogVolume_pos_of_measure_gt_one | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean | |
| additiveHaarFineLocalPayloadAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarFormulaGapLocalEstimateAuditThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarLocalAnalyticConstructionFormulaSourceEndpoint | Checked | unowned | Iut/Stage1/IUTStage1Experiments/AdditiveHaar.lean | |
| additiveHaarLocalArithmeticMatchingConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarLocalArithmeticMatchingConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarLocalizedDeterminantMultiplicityMatchesIUTIVCoefficient | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additive_haar_local_normalization_constructed_proof | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additive_haar_local_normalization_constructed_proof | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarPadicPrimeErrorDefectMainSplitConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarPadicPrimeErrorFormulaMatchingEndpointThreaded | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarProjectionEndpoint | Checked | unowned | Iut/Stage1/IUTStage1IUTIVAlgebra.lean | |
| additiveHaarRealifiedPacketSourceSuppliesStepXEqualities | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarResidualPayloadAudit_ofArithmeticSource | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveHaarStepXIArithmeticDegreeCalibrationConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarStrongestEndpointHasRemainingPayloadAudit | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveHaarTheorem110LocalAnalyticConstructed | Checked | unowned | Iut/Stage1/IUTStage1Theorem311.lean | |
| additiveLogVolume | Checked | unowned | Iut/Stage1/IUTStage1StepXI/Core.lean | |
| additiveLogVolume | Checked | unowned | Iut/Stage1/IUTStage1SourceCore.lean |
No theorems match the active view.
Showing the highest-priority 200 proofs for fast server render.