PaperFormalizer · Formalized papers
Formalized papers
Reconstruction from Milnor K-theory modulo the characteristic
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/OaiReconstructionMilnorTheory/Basic.lean
Papers/OaiReconstructionMilnorTheory/Helpers/CompatibleOperations.lean
Papers/OaiReconstructionMilnorTheory/Helpers/FieldGeometry.lean
Papers/OaiReconstructionMilnorTheory/Helpers/FieldReconstruction.lean
Papers/OaiReconstructionMilnorTheory/Helpers/InducedMaps.lean
Papers/OaiReconstructionMilnorTheory/Helpers/Intersection.lean
Papers/OaiReconstructionMilnorTheory/Helpers/IntersectionSetup.lean
Papers/OaiReconstructionMilnorTheory/Helpers/IntersectionSpectrum.lean
Papers/OaiReconstructionMilnorTheory/Helpers/Isomorphisms.lean
Papers/OaiReconstructionMilnorTheory/Helpers/LineRecoveryAffine.lean
Papers/OaiReconstructionMilnorTheory/Helpers/LineRecoveryAssembly.lean
Papers/OaiReconstructionMilnorTheory/Helpers/LineRecoveryContainment.lean
Papers/OaiReconstructionMilnorTheory/Helpers/LineRecoveryGeometry.lean
Papers/OaiReconstructionMilnorTheory/Helpers/LineRecoveryPropagation.lean
Papers/OaiReconstructionMilnorTheory/Helpers/Lines.lean
Papers/OaiReconstructionMilnorTheory/Helpers/MilnorProjective.lean
Papers/OaiReconstructionMilnorTheory/Helpers/NormalizedLift.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PBasis.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PDegree.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PDegreeFrobenius.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PDegreeMonomials.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PDegreeRational.lean
Papers/OaiReconstructionMilnorTheory/Helpers/PerfectCore.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveAffine.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveAssembly.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveCoordinates.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveField.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveFrame.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveIncidence.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveLift.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ProjectiveLiftBasic.lean
Papers/OaiReconstructionMilnorTheory/Helpers/ScalarLine.lean
Papers/OaiReconstructionMilnorTheory/Helpers/SymbolPairing.lean
Papers/OaiReconstructionMilnorTheory/Helpers/Symbols.lean
Papers/OaiReconstructionMilnorTheory/Helpers.lean
Papers/OaiReconstructionMilnorTheory/TMain.lean
Papers/OaiReconstructionMilnorTheory.lean
Papers.lean
README.md
lakefile.toml
lean-toolchain