`OAI/Geometry/HeilbronnTriangle/`

1953 declarations, 0 contain sorry, 0 declared as axioms; 242 files

Files

ActualPointLaw.lean 4 declarations
ActualPointLawBounds.lean 3 declarations
ActualPointLawTriples.lean 7 declarations
ActualWeightedFiberCount.lean 2 declarations
AffineShellCount.lean 2 declarations
AffineTripleOrbit.lean 18 declarations
AllowedShifts.lean 27 declarations
AlterationAsymptotics.lean 12 declarations
AnisotropicCount.lean 10 declarations
AnisotropicDyadic.lean 8 declarations
AnisotropicEstimate.lean 3 declarations
AnisotropicGeometry.lean 4 declarations
AnisotropicPlaneData.lean 3 declarations
Auxiliaries.lean 132 imports, no declarations
AuxiliaryAffineWeights.lean 11 declarations
AuxiliaryCap.lean 19 declarations
AuxiliaryIntegralSupport.lean 3 declarations
AuxiliarySamplingLaw.lean 4 declarations
AuxiliarySamplingParameters.lean 9 declarations
AuxiliarySamplingSupport.lean 5 declarations
AuxiliarySet.lean 15 declarations
AuxiliarySpecialRankTwo.lean 1 declarations
AuxiliarySupport.lean 2 declarations
AuxiliaryThreeCase.lean 10 declarations
AuxiliaryWeights.lean 21 declarations
AuxiliaryZeroCount.lean 3 declarations
AuxiliaryZeroWeights.lean 4 declarations
AveragedBadTripleBound.lean 2 declarations
BadTripleAverage.lean 4 declarations
CRTLifting.lean 37 declarations
CapInBox.lean 10 declarations
ConditionalBadTripleBound.lean 5 declarations
ConditionalDigits.lean 7 declarations
ConditionalMatrix.lean 16 declarations
ConditionalSamples.lean 12 declarations
ConditionalSmith.lean 3 declarations
CrossNormal.lean 6 declarations
Definitions.lean 12 declarations
Deletion.lean 3 declarations
DesignatedCoefficient.lean 8 declarations
DeterminantCoefficients.lean 13 declarations
DeterminantFibers.lean 5 declarations
DeterminantResidue.lean 12 declarations
DiagonalDetImage.lean 19 declarations
DiagonalKernel.lean 13 declarations
DiagonalStabilizer.lean 17 declarations
DigitBadTripleAverage.lean 11 declarations
DigitColumnLaw.lean 12 declarations
DigitEncoding.lean 2 declarations
DigitObstruction.lean 12 declarations
DigitUniqueness.lean 6 declarations
DigitUnits.lean 13 declarations
DividingPivot.lean 6 declarations
DivisorMoment.lean 6 declarations
EncodedDeterminant.lean 3 declarations
EqualCoordinatePacking.lean 9 declarations
EqualCoordinatePlane.lean 7 declarations
ExactPlaneCovolume.lean 5 declarations
ExponentScaling.lean 1 declarations
FinalSampling.lean 2 declarations
FinalScaling.lean 3 declarations
FinalScalingBridge.lean 3 declarations
FiniteFieldLabels.lean 8 declarations
FiniteIndexPlane.lean 5 declarations
FiniteMixtures.lean 5 declarations
FixedDetLattice.lean 11 declarations
FixedDetReduction.lean 9 declarations
FullIntegralLattice.lean 1 declarations
GcdPairCount.lean 3 declarations
GeometricAlteration.lean 3 declarations
HomogeneousGeometry.lean 9 declarations
IndependentColumns.lean 3 declarations
IndependentTupleCard.lean 5 declarations
IntegerMatrixEvents.lean 17 declarations
IntegerMatrixFibers.lean 11 declarations
IntegerMatrixTransport.lean 30 declarations
IntegerMixtureGeometry.lean 1 declarations
IntegerNormalGroups.lean 4 declarations
IntegerPlaneEstimates.lean 29 declarations
IntegerPointLaw.lean 3 declarations
IntegerPointLawPairs.lean 2 declarations
IntegerPointLawTriples.lean 8 declarations
IntegerSampleMixtures.lean 16 declarations
IntegerSampling.lean 11 declarations
IntegerSamplingGeometry.lean 12 declarations
IntegerSamplingPairs.lean 14 declarations
IntegerSharedCollisions.lean 3 declarations
IntegralAmbientLattice.lean 10 declarations
IntegralKernelMoment.lean 5 declarations
IntegralPlaneDeterminant.lean 3 declarations
IntegralPlaneLattice.lean 49 declarations
IntegralPlaneMatrixCount.lean 3 declarations
IntegralPlaneReduction.lean 13 declarations
IntegralPlaneRows.lean 6 declarations
LabelResidues.lean 7 declarations
LatticeBox.lean 12 declarations
LatticeCoordinates.lean 15 declarations
LatticeLowerProduct.lean 5 declarations
LatticeMoment.lean 2 declarations
LatticePacking.lean 12 declarations
LatticeReciprocal.lean 5 declarations
LatticeResidues.lean 10 declarations
LatticeShell.lean 9 declarations
LatticeSplit.lean 31 declarations
LiftCollisions.lean 17 declarations
LiftedBadEvent.lean 4 declarations
LiftingProbability.lean 29 declarations
Main.lean 2 declarations
MainDigitBadTripleBound.lean 4 declarations
MainDigitCollision.lean 5 declarations
MainDigitLaw.lean 17 declarations
MainDigitObstruction.lean 4 declarations
MainDigitOrbitObstruction.lean 7 declarations
MainOrbitObstruction.lean 6 declarations
MainResidueSystem.lean 4 declarations
MatrixAffineShell.lean 2 declarations
MatrixAuxiliaryWeights.lean 11 declarations
MatrixSpecialRankTwo.lean 5 declarations
MinorInvariant.lean 11 declarations
MixtureLifting.lean 7 declarations
MonomialCount.lean 18 declarations
NonzeroAuxiliaryCount.lean 4 declarations
NonzeroWeightedCount.lean 16 declarations
NormDecomposition.lean 10 declarations
NormDeterminant.lean 18 declarations
NormEncoding.lean 20 declarations
NormFoundation.lean 6 declarations
NormHomogeneity.lean 10 declarations
NormPolynomial.lean 12 declarations
NormalFiberCount.lean 5 declarations
NormalGroupCount.lean 3 declarations
OrbitCardinality.lean 8 declarations
OrbitEstimate.lean 4 declarations
OrbitProbabilityBound.lean 3 declarations
OrbitRowLattice.lean 8 declarations
OrbitSampling.lean 12 declarations
OrbitSamplingCardinality.lean 4 declarations
OrbitUniform.lean 4 declarations
PairingDivisor.lean 10 declarations
PairingMoment.lean 2 declarations
ParameterConclusion.lean 4 declarations
ParameterSampling.lean 7 declarations
ParameterSequence.lean 30 declarations
Parameters.lean 23 declarations
PivotAssembly.lean 9 declarations
PlaneBasisIndex.lean 13 declarations
PlaneCount.lean 7 declarations
PlaneCovolume.lean 11 declarations
PlaneDeterminant.lean 3 declarations
PlaneFiberAssembly.lean 3 declarations
PlaneFunctional.lean 4 declarations
PlaneIndex.lean 2 declarations
PlaneLineMatrices.lean 5 declarations
PlaneLines.lean 13 declarations
PlaneLowRankCount.lean 6 declarations
PlaneMatrixCount.lean 2 declarations
PlaneRadius.lean 2 declarations
PlaneReduction.lean 8 declarations
PlaneRowTransport.lean 20 declarations
PlaneTripleCount.lean 3 declarations
PlaneWeightedLines.lean 3 declarations
PointLawBadTripleBound.lean 4 declarations
PolynomialCoefficients.lean 27 declarations
PowerGap.lean 1 declarations
PrescribedDigits.lean 6 declarations
PrimeLiftParameters.lean 9 declarations
PrimeParameters.lean 8 declarations
PrimePowerData.lean 10 declarations
PrimePowerFactors.lean 6 declarations
PrimePowerGL.lean 14 declarations
PrimePowerRowData.lean 13 declarations
PrimePowerStabilizer.lean 2 declarations
PrimitiveLine.lean 5 declarations
PrimitiveNormal.lean 29 declarations
PrimitiveVector.lean 3 declarations
ProjectiveBadEvent.lean 6 declarations
ProportionalPairs.lean 17 declarations
RandomAlteration.lean 4 declarations
RankOneMinors.lean 5 declarations
RealPlaneReduction.lean 9 declarations
Refutation.lean 1 declarations
RepeatedLabels.lean 5 declarations
RowLattice.lean 20 declarations
RowLatticeDuality.lean 7 declarations
RowLatticeEqualShell.lean 1 declarations
RowLatticeFixedDet.lean 7 declarations
RowLatticeMatrices.lean 14 declarations
RowLatticeMoment.lean 5 declarations
RowLatticePlane.lean 10 declarations
RowLatticeVolume.lean 5 declarations
RowPairingDivisor.lean 5 declarations
RowPlaneReduction.lean 5 declarations
SampleDeletion.lean 7 declarations
SampleUpper.lean 3 declarations
SamplingBound.lean 2 declarations
SamplingErrors.lean 7 declarations
SharedGeometricAlteration.lean 7 declarations
ShortKernelVectors.lean 5 declarations
ShortRelations.lean 4 declarations
ShortestIntegralVector.lean 9 declarations
SmallDeterminantReduction.lean 4 declarations
SmallDeterminantWeight.lean 9 declarations
SmithAffineShell.lean 1 declarations
SmithDigitMoment.lean 4 declarations
SmithEqualShell.lean 1 declarations
SmithPlaneData.lean 3 declarations
SmithSpecialRankTwo.lean 1 declarations
SpecialNormalShell.lean 4 declarations
SpecialNormals.lean 8 declarations
SpecialRankOneCount.lean 2 declarations
SpecialRankTwo.lean 7 declarations
StabilizerConjugation.lean 5 declarations
SuccessiveBox.lean 4 declarations
SuccessiveEstimates.lean 4 declarations
SuccessiveMinima.lean 2 declarations
SuccessivePair.lean 2 declarations
SuccessiveTransport.lean 2 declarations
SuccessiveVectors.lean 10 declarations
TranslateAverage.lean 5 declarations
TripleEnumeration.lean 13 declarations
TwoByTwoPivot.lean 6 declarations
TwoByTwoSmith.lean 4 declarations
TypedFixedFiberCount.lean 7 declarations
UniformAction.lean 7 declarations
UniformFixedFiberCount.lean 13 declarations
UniformLiftPairs.lean 3 declarations
UnitRowLatticeMoment.lean 3 declarations
WeightedNormalReduction.lean 5 declarations
WeightedZeroAssembly.lean 4 declarations
WeightedZeroPartition.lean 10 declarations
ZModAnnihilator.lean 7 declarations
ZeroAffineShell.lean 7 declarations
ZeroCombinedShell.lean 5 declarations
ZeroCountNormalization.lean 6 declarations
ZeroDeterminantCount.lean 15 declarations
ZeroEqualAdditional.lean 3 declarations
ZeroEqualMatrices.lean 1 declarations
ZeroGlobalCount.lean 3 declarations
ZeroMomentSum.lean 3 declarations
ZeroNormalDyadic.lean 3 declarations
ZeroRowData.lean 8 declarations
ZeroThreeCasePartition.lean 7 declarations