Commit b08bce4

committed

Merge branch 'master' into aliu/krullTopology

2 parents 6508683 + 06a46da commit b08bce4Copy full SHA for b08bce4

3,573 files changed

+82080

-39448

lines changed

.github
- actions/get-mathlib-ci
  - README.md
  - action.yml
- workflows
.gitignore
Archive
- Examples
  - Eisenstein.lean
  - PropEncodable.lean
- Hairer.lean
- Imo
- MinimalSheffer.lean
- MiuLanguage
- Sensitivity.lean
- Wiedijk100Theorems
Cache
Counterexamples
Mathlib.lean
Mathlib
- AlgebraicGeometry
- AlgebraicTopology
  - DoldKan
  - ExtraDegeneracy.lean
  - FundamentalGroupoid
    - Basic.lean
    - Product.lean
  - ModelCategory
  - Quasicategory
    - Basic.lean
    - StrictBicategory.lean
  - RelativeCellComplex
    - AttachCells.lean
  - SimplexCategory
    - Augmented
      - Basic.lean
      - Monoidal.lean
    - Basic.lean
    - GeneratorsRelations
      - Basic.lean
      - EpiMono.lean
    - ToMkOne.lean
  - SimplicialComplex
    - Basic.lean
  - SimplicialObject
  - SimplicialSet
  - SingularHomology
    - HomotopyInvariance.lean
  - SingularSet.lean
  - TopologicalSimplex.lean
- Algebra
  - AddConstMap
    - Basic.lean
  - AffineMonoid
    - Embedding.lean
  - Algebra
    - Basic.lean
    - Epi.lean
    - Equiv.lean
    - Hom.lean
    - NonUnitalSubalgebra.lean
    - Operations.lean
    - Pi.lean
    - RestrictScalars.lean
    - Spectrum
      - Basic.lean
      - Quasispectrum.lean
    - StrictPositivity.lean
    - Subalgebra
    - Unitization.lean
    - ZMod.lean
  - Azumaya
    - Matrix.lean
  - BigOperators
    - Expect.lean
    - Field.lean
    - Fin.lean
    - Finprod.lean
    - Group/Finset
      - Basic.lean
      - Gaps.lean
  - BrauerGroup
    - Defs.lean
  - Category
    - AlgCat
    - CommAlgCat
      - Basic.lean
    - FGModuleCat
    - Grp
    - HopfAlgCat
      - Monoidal.lean
    - ModuleCat
    - MonCat
    - Ring
  - CharP
    - Basic.lean
    - Defs.lean
    - Invertible.lean
    - MixedCharZero.lean
    - Quotient.lean
    - Two.lean
  - Colimit
    - Ring.lean
  - ContinuedFractions
    - Basic.lean
    - Computation
  - DirectSum
    - Basic.lean
    - Decomposition.lean
    - Finsupp.lean
    - Internal.lean
    - Module.lean
    - Ring.lean
  - DualNumber.lean
  - DualQuaternion.lean
  - EuclideanDomain
    - Int.lean
  - Exact.lean
  - Expr.lean
  - Field
    - Basic.lean
    - Equiv.lean
    - IsField.lean
    - Subfield
      - Basic.lean
      - Defs.lean
  - FiniteSupport
    - Basic.lean
    - Defs.lean
  - FreeAlgebra.lean
  - FreeMonoid
    - Basic.lean
  - GCDMonoid
    - Basic.lean
    - Finset.lean
    - Nat.lean
  - GradedMonoid.lean
  - GroupWithZero
    - Action
      - Defs.lean
    - Associated.lean
    - Basic.lean
    - Commute.lean
    - InjSurj.lean
    - Invertible.lean
    - Range.lean
    - Units
      - Basic.lean
      - Lemmas.lean
  - Group
    - Action
      - Basic.lean
      - Defs.lean
      - End.lean
      - Faithful.lean
      - Pointwise
        Finset.lean
        Set
        Basic.lean
    - AddChar.lean
    - Commutator.lean
    - Commute
      - Defs.lean
    - Conj.lean
    - Defs.lean
    - End.lean
    - Equiv
      - TypeTags.lean
    - Fin
      - Basic.lean
    - Hom
      - Basic.lean
      - Defs.lean
      - End.lean
      - Instances.lean
    - Idempotent.lean
    - InjSurj.lean
    - Invertible
      - Basic.lean
      - Defs.lean
    - Irreducible
      - Indecomposable.lean
    - NatPowAssoc.lean
    - Opposite.lean
    - Pi
      - Basic.lean
    - Pointwise
      - Finset
        Basic.lean
        Scalar.lean
      - Set
        Basic.lean
        Scalar.lean
    - Semiconj
      - Defs.lean
    - Subgroup
      - Actions.lean
      - Basic.lean
      - Defs.lean
      - Finite.lean
      - Ker.lean
      - Map.lean
      - MulOpposite.lean
      - Pointwise.lean
      - ZPowers
        Basic.lean
        Lemmas.lean
    - Submonoid
      - Basic.lean
      - Defs.lean
      - Operations.lean
      - Pointwise.lean
      - Saturation.lean
      - Support.lean
      - Units.lean
    - TransferInstance.lean
    - TypeTags
      - Hom.lean
    - ULift.lean
    - Units
      - Defs.lean
    - WithOne
      - Basic.lean
  - HierarchyDesign.lean
  - Homology
    - Additive.lean
    - Augment.lean
    - BifunctorShift.lean
    - CochainComplexPlus.lean
    - CommSq.lean
    - ComplexShapeSigns.lean
    - DerivedCategory
      - Basic.lean
      - Ext
        ExtClass.lean
        Map.lean
        TStructure.lean
      - HomologySequence.lean
      - ShortExact.lean
      - SingleTriangle.lean
    - Embedding
      - Basic.lean
      - ExtendHomology.lean
      - ExtendHomotopy.lean
    - ExactSequenceFour.lean
    - Factorizations
      - CM5a.lean
    - Functor.lean
    - GrothendieckAbelian.lean
    - HomologicalBicomplex.lean
    - HomologicalComplexAbelian.lean
    - Homotopy.lean
    - HomotopyCategory.lean
    - HomotopyCategory
      - HomComplex.lean
      - HomComplexCohomology.lean
      - HomComplexSingle.lean
      - Pretriangulated.lean
      - Shift.lean
      - ShortExact.lean
      - SingleFunctors.lean
    - Linear.lean
    - Localization.lean
    - ModelCategory
      - Lifting.lean
    - Opposite.lean
    - ShortComplex
      - Ab.lean
      - Abelian.lean
      - ExactFunctor.lean
      - Homology.lean
      - LeftHomology.lean
      - Limits.lean
      - ModuleCat.lean
      - RightHomology.lean
    - Single.lean
    - SpectralObject
      - Basic.lean
      - Differentials.lean
      - EpiMono.lean
      - HasSpectralSequence.lean
      - Homology.lean
      - Page.lean
      - SpectralSequence.lean
  - Jordan
    - Basic.lean
  - LieRinehartAlgebra
    - Defs.lean
  - Lie
    - AdjointAction
      - Basic.lean
      - Derivation.lean
    - Basic.lean
    - Basis.lean
    - CartanExists.lean
    - Classical.lean
    - Derivation
      - BaseChange.lean
      - Basic.lean
      - Killing.lean
    - DirectSum.lean
    - Engel.lean
    - EngelSubalgebra.lean
    - Extension.lean
    - Free.lean
    - IdealOperations.lean
    - Loop.lean
    - Nilpotent.lean
    - NonUnitalNonAssocAlgebra.lean
    - Normalizer.lean
    - Prod.lean
    - Quotient.lean
    - SemiDirect.lean
    - SkewAdjoint.lean
    - Subalgebra.lean
    - Submodule.lean
    - TraceForm.lean
    - UniversalEnveloping.lean
    - Weights
      - Cartan.lean
      - IsSimple.lean
      - Killing.lean
  - LinearRecurrence.lean
  - Module
    - CharacterModule.lean
    - Congruence
      - Defs.lean
    - DedekindDomain.lean
    - Equiv
      - Basic.lean
    - FinitePresentation.lean
    - GradedModule.lean
    - Hom.lean
    - LinearMap
      - Basic.lean
      - Defs.lean
      - Polynomial.lean
    - LocalizedModule
      - Basic.lean
    - NatInt.lean
    - PID.lean
    - PUnit.lean
    - Presentation
      - Basic.lean
      - Cokernel.lean
      - DirectSum.lean
      - Finite.lean
    - SnakeLemma.lean
    - SpanRank.lean
    - SpanRankOperations.lean
    - Submodule
      - Defs.lean
      - Equiv.lean
      - Lattice.lean
      - Pointwise.lean
      - Range.lean
      - Union.lean
    - Torsion
      - Basic.lean
    - ULift.lean
    - ZLattice
      - Basic.lean
      - Covolume.lean
      - Summable.lean
  - MonoidAlgebra
    - Basic.lean
    - Cardinal.lean
    - Defs.lean
    - Degree.lean
    - Grading.lean
    - MapDomain.lean
    - Module.lean
  - MvPolynomial
    - Basic.lean
    - Cardinal.lean
    - Coeff.lean
    - CommRing.lean
    - Degrees.lean
    - Equiv.lean
    - Eval.lean
    - Nilpotent.lean
    - PDeriv.lean
    - Rename.lean
    - SchwartzZippel.lean
    - Variables.lean
  - NonAssoc/LieAdmissible
    - Defs.lean
  - Notation.lean
  - Notation
    - Defs.lean
    - Lemmas.lean
    - Pi
      - Defs.lean
    - Prod.lean
  - Order
    - AbsoluteValue
      - Basic.lean
    - Algebra.lean
    - Antidiag
      - FinsuppEquiv.lean
      - Prod.lean
    - Archimedean
      - Basic.lean
      - Class.lean
    - BigOperators
      - GroupWithZero
        Finset.lean
      - Group
        Finset.lean
    - CompleteField.lean
    - Field
      - Basic.lean
      - Rat.lean
    - Floor
      - Defs.lean
      - Extended.lean
      - Ring.lean
      - Semifield.lean
    - GroupWithZero
      - Action
        Synonym.lean
      - Finset.lean
      - Range.lean
      - Synonym.lean
      - Unbundled
        Basic.lean
    - Group
      - Action
        Synonym.lean
      - Cone.lean
      - Lattice.lean
      - PartialSups.lean
      - Pointwise
        Interval.lean
      - Synonym.lean
      - Unbundled
        Abs.lean
        Int.lean
    - Hom
      - Basic.lean
      - Monoid.lean
      - TypeTags.lean
    - Interval
      - Basic.lean
    - Invertible.lean
    - Module
      - HahnEmbedding.lean
      - PositiveLinearMap.lean
      - Synonym.lean
    - Monoid
      - Canonical
        Defs.lean
      - Unbundled
        Basic.lean
        WithTop.lean
    - Monovary.lean
    - Nonneg
      - Field.lean
      - Lattice.lean
    - Rearrangement.lean
    - Ring
      - Abs.lean
      - Archimedean.lean
      - Cast.lean
      - Cone.lean
      - GeomSum.lean
      - IsNonarchimedean.lean
      - StandardPart.lean
      - Synonym.lean
      - Unbundled
        Rat.lean
      - WithTop.lean
    - Star
      - Basic.lean
    - SuccPred.lean
    - SuccPred
      - TypeTags.lean
      - WithBot.lean
    - UpperLower.lean
  - Polynomial
    - AlgebraMap.lean
    - Basic.lean
    - BigOperators.lean
    - Bivariate.lean
    - Degree
      - Defs.lean
      - SmallDegree.lean
      - TrailingDegree.lean
    - Derivative.lean
    - EraseLead.lean
    - Eval
      - Defs.lean
    - HasseDeriv.lean
    - Homogenize.lean
    - Inductions.lean
    - Laurent.lean
    - Mirror.lean
    - Module
      - Basic.lean
    - PartialFractions.lean
    - RuleOfSigns.lean
    - Sequence.lean
    - Smeval.lean
    - Splits.lean
    - UnitTrinomial.lean
  - PresentedMonoid
    - Basic.lean
  - QuadraticAlgebra
    - Defs.lean
  - Quandle.lean
  - Quaternion.lean
  - Quotient.lean
  - Regular
    - SMul.lean
  - Ring
    - Action
      - Subobjects.lean
    - CentroidHom.lean
    - Defs.lean
    - GeomSum.lean
    - InjSurj.lean
    - Invertible.lean
    - Prod.lean
    - Semireal
      - Defs.lean
    - Subring
    - Subsemiring
      - Defs.lean
    - ULift.lean
  - SkewMonoidAlgebra
    - Basic.lean
  - Squarefree
    - Basic.lean
  - Star
    - Basic.lean
    - NonUnitalSubalgebra.lean
    - Prod.lean
    - RingQuot.lean
    - SelfAdjoint.lean
    - StarAlgHom.lean
    - Subalgebra.lean
    - Unitary.lean
  - TrivSqZeroExt
    - Basic.lean
  - Tropical
    - Lattice.lean
  - Vertex
    - HVertexOperator.lean
    - VertexOperator.lean
  - WithConv.lean
- Analysis
  - AbsoluteValue
    - Equivalence.lean
  - Analytic
  - Asymptotics
  - BoxIntegral
    - Basic.lean
    - Box
      - Basic.lean
    - Partition
      - Filter.lean
  - CStarAlgebra

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Commit b08bce4

3,573 files changed

File tree

3,573 files changed