Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-10 05:56
777eb7c4
View on Github →
chore: bump toolchain to v4.29.0-rc6 (
#36422
)
Estimated changes
Modified
Archive/Imo/Imo2019Q2.lean
Modified
Archive/MinimalSheffer.lean
Modified
Mathlib/Algebra/Algebra/ZMod.lean
Modified
Mathlib/Algebra/BrauerGroup/Defs.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Colimits.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Limits.lean
Modified
Mathlib/Algebra/Category/Grp/Abelian.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Abelian.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Descent.lean
Modified
Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
Modified
Mathlib/Algebra/CharP/Invertible.lean
Modified
Mathlib/Algebra/CharP/MixedCharZero.lean
Modified
Mathlib/Algebra/DirectSum/Decomposition.lean
Modified
Mathlib/Algebra/Expr.lean
Modified
Mathlib/Algebra/Field/IsField.lean
Modified
Mathlib/Algebra/FreeMonoid/Basic.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.lean
Modified
Mathlib/Algebra/Group/Action/Basic.lean
Modified
Mathlib/Algebra/Group/Action/Defs.lean
Modified
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
Modified
Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean
Modified
Mathlib/Algebra/Group/Hom/Basic.lean
Modified
Mathlib/Algebra/Group/Invertible/Basic.lean
Modified
Mathlib/Algebra/Group/Invertible/Defs.lean
Modified
Mathlib/Algebra/Group/Pi/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean
Modified
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean
Modified
Mathlib/Algebra/Group/Submonoid/Pointwise.lean
Modified
Mathlib/Algebra/Group/Units/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/InjSurj.lean
Modified
Mathlib/Algebra/GroupWithZero/Invertible.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
Modified
Mathlib/Algebra/Homology/ComplexShapeSigns.lean
Modified
Mathlib/Algebra/Lie/Basic.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/Lie/Extension.lean
Modified
Mathlib/Algebra/Module/GradedModule.lean
Modified
Mathlib/Algebra/Module/NatInt.lean
Modified
Mathlib/Algebra/Module/Submodule/Defs.lean
Modified
Mathlib/Algebra/Module/Torsion/Basic.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Module.lean
Modified
Mathlib/Algebra/Order/Archimedean/Basic.lean
Modified
Mathlib/Algebra/Order/Floor/Defs.lean
Modified
Mathlib/Algebra/Order/Group/Lattice.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
Modified
Mathlib/Algebra/Ring/Invertible.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/Star/RingQuot.lean
Modified
Mathlib/AlgebraicGeometry/Cover/Directed.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Matrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
Modified
Mathlib/Analysis/Distribution/TestFunction.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Defs.lean
Modified
Mathlib/Analysis/InnerProductSpace/OfNorm.lean
Modified
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
Modified
Mathlib/Analysis/Matrix/Order.lean
Modified
Mathlib/Analysis/Matrix/PosDef.lean
Modified
Mathlib/Analysis/Normed/Algebra/Exponential.lean
Modified
Mathlib/Analysis/Normed/Field/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/AddTorsor.lean
Modified
Mathlib/Analysis/Normed/Module/Basic.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
Modified
Mathlib/Analysis/RCLike/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
Modified
Mathlib/CategoryTheory/Abelian/Transfer.lean
Modified
Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean
Modified
Mathlib/CategoryTheory/CatCommSq.lean
Modified
Mathlib/CategoryTheory/Center/Linear.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Forget.lean
Modified
Mathlib/CategoryTheory/Enriched/Basic.lean
Modified
Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
Modified
Mathlib/CategoryTheory/EpiMono.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean
Modified
Mathlib/CategoryTheory/Functor/Functorial.lean
Modified
Mathlib/CategoryTheory/Groupoid.lean
Modified
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
Modified
Mathlib/CategoryTheory/IsConnected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/FullSubcategory.lean
Modified
Mathlib/CategoryTheory/Limits/MorphismProperty.lean
Modified
Mathlib/CategoryTheory/Limits/Preorder.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Localization/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
Modified
Mathlib/CategoryTheory/Localization/HasLocalization.lean
Modified
Mathlib/CategoryTheory/Localization/Linear.lean
Modified
Mathlib/CategoryTheory/Localization/LocallySmall.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Localization/Predicate.lean
Modified
Mathlib/CategoryTheory/Localization/Triangulated.lean
Modified
Mathlib/CategoryTheory/Localization/Trifunctor.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean
Modified
Mathlib/CategoryTheory/Monad/Comonadicity.lean
Modified
Mathlib/CategoryTheory/Monad/Limits.lean
Modified
Mathlib/CategoryTheory/Monad/Monadicity.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/Opposites.lean
Modified
Mathlib/CategoryTheory/Monoidal/Bimod.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Multifunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Complete.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Types.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Zero.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mod_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Multifunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
Modified
Mathlib/CategoryTheory/Monoidal/Transport.lean
Modified
Mathlib/CategoryTheory/Preadditive/Schur.lean
Modified
Mathlib/CategoryTheory/Preadditive/Transfer.lean
Modified
Mathlib/CategoryTheory/Quotient/Linear.lean
Modified
Mathlib/CategoryTheory/Quotient/Preadditive.lean
Modified
Mathlib/CategoryTheory/Shift/Adjunction.lean
Modified
Mathlib/CategoryTheory/Shift/Basic.lean
Modified
Mathlib/CategoryTheory/Shift/CommShift.lean
Modified
Mathlib/CategoryTheory/Shift/Induced.lean
Modified
Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
Modified
Mathlib/CategoryTheory/Shift/Localization.lean
Modified
Mathlib/CategoryTheory/Shift/Opposite.lean
Modified
Mathlib/CategoryTheory/Shift/ShiftSequence.lean
Modified
Mathlib/CategoryTheory/Sites/Limits.lean
Modified
Mathlib/CategoryTheory/Sites/Monoidal.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Basic.lean
Modified
Mathlib/CategoryTheory/Thin.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/AbelianSubcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean
Modified
Mathlib/Combinatorics/Configuration.lean
Modified
Mathlib/Combinatorics/Hindman.lean
Modified
Mathlib/Combinatorics/Quiver/Arborescence.lean
Modified
Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
Modified
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Trails.lean
Modified
Mathlib/Computability/Primrec/Basic.lean
Modified
Mathlib/Computability/Primrec/List.lean
Modified
Mathlib/Computability/TuringMachine/Tape.lean
Modified
Mathlib/Control/Functor/Multivariate.lean
Modified
Mathlib/Control/Monad/Writer.lean
Modified
Mathlib/Control/Traversable/Equiv.lean
Modified
Mathlib/Control/ULiftable.lean
Modified
Mathlib/Data/Analysis/Topology.lean
Modified
Mathlib/Data/FinEnum.lean
Modified
Mathlib/Data/FinEnum/Option.lean
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/Fintype/Card.lean
Modified
Mathlib/Data/Fintype/Defs.lean
Modified
Mathlib/Data/Fintype/EquivFin.lean
Modified
Mathlib/Data/Fintype/OfMap.lean
Modified
Mathlib/Data/Fintype/Option.lean
Modified
Mathlib/Data/Fintype/Perm.lean
Modified
Mathlib/Data/Fintype/Sets.lean
Modified
Mathlib/Data/Fintype/Sum.lean
Modified
Mathlib/Data/FunLike/Fintype.lean
Modified
Mathlib/Data/List/GetD.lean
Modified
Mathlib/Data/List/Rotate.lean
Modified
Mathlib/Data/Matrix/Invertible.lean
Modified
Mathlib/Data/QPF/Multivariate/Basic.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Quot.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Quot.lean
Modified
Mathlib/Data/Set/Countable.lean
Modified
Mathlib/Data/Set/Finite/Basic.lean
Modified
Mathlib/Data/Set/Finite/Lattice.lean
Modified
Mathlib/Data/Set/Finite/Monad.lean
Modified
Mathlib/Data/Setoid/Basic.lean
Modified
Mathlib/Data/Setoid/Partition.lean
Modified
Mathlib/Data/W/Basic.lean
Modified
Mathlib/Deprecated/Estimator.lean
Modified
Mathlib/Dynamics/Flow.lean
Modified
Mathlib/FieldTheory/Differential/Basic.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
Modified
Mathlib/FieldTheory/Finiteness.lean
Modified
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
Modified
Mathlib/FieldTheory/KrullTopology.lean
Modified
Mathlib/FieldTheory/Minpoly/Field.lean
Modified
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
Modified
Mathlib/FieldTheory/PolynomialGaloisGroup.lean
Modified
Mathlib/FieldTheory/RatFunc/Basic.lean
Modified
Mathlib/Geometry/Convex/Cone/Basic.lean
Modified
Mathlib/Geometry/Diffeology/Basic.lean
Modified
Mathlib/Geometry/Manifold/ChartedSpace.lean
Modified
Mathlib/Geometry/Manifold/HasGroupoid.lean
Modified
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean
Modified
Mathlib/GroupTheory/Coset/Defs.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/DoubleCoset.lean
Modified
Mathlib/GroupTheory/FixedPointFree.lean
Modified
Mathlib/GroupTheory/Index.lean
Modified
Mathlib/GroupTheory/Nilpotent.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/OreLocalization/Basic.lean
Modified
Mathlib/GroupTheory/PGroup.lean
Modified
Mathlib/GroupTheory/Perm/Centralizer.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Sign.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Finite.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/Subgroup/Center.lean
Modified
Mathlib/GroupTheory/Sylow.lean
Modified
Mathlib/GroupTheory/Torsion.lean
Modified
Mathlib/LinearAlgebra/Basis/Defs.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
Modified
Mathlib/LinearAlgebra/Dimension/Finite.lean
Modified
Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
Modified
Mathlib/LinearAlgebra/Matrix/Basis.lean
Modified
Mathlib/LinearAlgebra/Matrix/Block.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Projective.lean
Modified
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean
Modified
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
Modified
Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
Modified
Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Defs.lean
modified
def
RootPairing.indexNeg
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
modified
def
RootPairing.EmbeddedG2.ofPairingInThree
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Denumerable.lean
Modified
Mathlib/Logic/Encodable/Basic.lean
Modified
Mathlib/Logic/Equiv/List.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/Logic/Unique.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/Cylinders.lean
Modified
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
Modified
Mathlib/MeasureTheory/Function/AEEqFun.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
Modified
Mathlib/MeasureTheory/PiSystem.lean
Modified
Mathlib/ModelTheory/Basic.lean
Modified
Mathlib/ModelTheory/Equivalence.lean
Modified
Mathlib/ModelTheory/Graph.lean
Modified
Mathlib/ModelTheory/LanguageMap.lean
Modified
Mathlib/ModelTheory/Order.lean
Modified
Mathlib/NumberTheory/ClassNumber/Finite.lean
Modified
Mathlib/NumberTheory/FunctionField.lean
Modified
Mathlib/NumberTheory/ModularForms/Delta.lean
Modified
Mathlib/NumberTheory/ModularForms/SlashActions.lean
Modified
Mathlib/Order/Antisymmetrization.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/BooleanAlgebra/Defs.lean
Modified
Mathlib/Order/BooleanGenerators.lean
Modified
Mathlib/Order/Comparable.lean
Modified
Mathlib/Order/Compare.lean
Modified
Mathlib/Order/CompleteBooleanAlgebra.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
Modified
Mathlib/Order/Copy.lean
Modified
Mathlib/Order/Defs/PartialOrder.lean
Modified
Mathlib/Order/DirectedInverseSystem.lean
Modified
Mathlib/Order/Extension/Well.lean
Modified
Mathlib/Order/Filter/Germ/Basic.lean
Modified
Mathlib/Order/Filter/Pointwise.lean
Modified
Mathlib/Order/GaloisConnection/Defs.lean
Modified
Mathlib/Order/Interval/Finset/Basic.lean
Modified
Mathlib/Order/Interval/Finset/Defs.lean
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/OrderDual.lean
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/SuccPred/Basic.lean
Modified
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
Modified
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
Modified
Mathlib/Order/SupClosed.lean
Modified
Mathlib/Order/Types/Defs.lean
Modified
Mathlib/Order/WellFounded.lean
Modified
Mathlib/Probability/Process/Predictable.lean
Modified
Mathlib/Probability/Process/Stopping.lean
Modified
Mathlib/RingTheory/AlgebraTower.lean
Modified
Mathlib/RingTheory/Bialgebra/Basic.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Modified
Mathlib/RingTheory/EuclideanDomain.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Basic.lean
Modified
Mathlib/RingTheory/IdealFilter/Topology.lean
Modified
Mathlib/RingTheory/IntegralDomain.lean
Modified
Mathlib/RingTheory/Invariant/Basic.lean
Modified
Mathlib/RingTheory/LittleWedderburn.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/Localization/Defs.lean
Modified
Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
Modified
Mathlib/RingTheory/NonUnitalSubring/Basic.lean
Modified
Mathlib/RingTheory/OreLocalization/OreSet.lean
Modified
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
Modified
Mathlib/RingTheory/PowerBasis.lean
Modified
Mathlib/RingTheory/PrincipalIdealDomain.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Finite.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/GCDMonoid.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
Modified
Mathlib/RingTheory/Valuation/Basic.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/RankOne.lean
Modified
Mathlib/RingTheory/Valuation/RankOne.lean
Modified
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
Modified
Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Basic.lean
Modified
Mathlib/Tactic/Inhabit.lean
Modified
Mathlib/Tactic/Linarith/Preprocessing.lean
Modified
Mathlib/Tactic/NormNum/Basic.lean
Modified
Mathlib/Tactic/NormNum/Result.lean
Modified
Mathlib/Topology/Algebra/FilterBasis.lean
Modified
Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
Modified
Mathlib/Topology/Algebra/UniformFilterBasis.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Bornology/Basic.lean
Modified
Mathlib/Topology/CWComplex/Classical/Basic.lean
Modified
Mathlib/Topology/CWComplex/Classical/Finite.lean
Modified
Mathlib/Topology/Category/CompHausLike/Cartesian.lean
Modified
Mathlib/Topology/Compactness/Compact.lean
Modified
Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
Modified
Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
Modified
Mathlib/Topology/Compactness/LocallyFinite.lean
Modified
Mathlib/Topology/Compactness/SigmaCompact.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/Connected/PathConnected.lean
Modified
Mathlib/Topology/Convenient/GeneratedBy.lean
Modified
Mathlib/Topology/Defs/Filter.lean
Modified
Mathlib/Topology/Defs/Induced.lean
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
Modified
Mathlib/Topology/FiberBundle/Basic.lean
Modified
Mathlib/Topology/FiberBundle/Constructions.lean
Modified
Mathlib/Topology/Homotopy/HSpaces.lean
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/MetricSpace/Defs.lean
Modified
Mathlib/Topology/MetricSpace/Gluing.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Topology/Metrizable/CompletelyMetrizable.lean
Modified
Mathlib/Topology/Metrizable/Uniformity.lean
Modified
Mathlib/Topology/Order.lean
Modified
Mathlib/Topology/Order/Basic.lean
Modified
Mathlib/Topology/Order/Bornology.lean
Modified
Mathlib/Topology/Order/LawsonTopology.lean
Modified
Mathlib/Topology/Order/LowerUpperTopology.lean
Modified
Mathlib/Topology/Order/ScottTopology.lean
Modified
Mathlib/Topology/Order/UpperLowerSetTopology.lean
Modified
Mathlib/Topology/Separation/Basic.lean
Modified
Mathlib/Topology/Separation/Hausdorff.lean
Modified
Mathlib/Topology/Sets/Closeds.lean
Modified
Mathlib/Topology/Sets/Opens.lean
Modified
Mathlib/Topology/Spectral/ConstructibleTopology.lean
Modified
Mathlib/Topology/UniformSpace/AbsoluteValue.lean
Modified
Mathlib/Topology/UniformSpace/Defs.lean
Modified
Mathlib/Topology/UniformSpace/OfCompactT2.lean
Modified
Mathlib/Topology/UniformSpace/OfFun.lean
Modified
Mathlib/Topology/UniformSpace/UniformEmbedding.lean
Modified
Mathlib/Topology/VectorBundle/Basic.lean
Modified
MathlibTest/DeriveFintype.lean
Modified
MathlibTest/MinImports.lean
Modified
MathlibTest/Simps.lean
Modified
MathlibTest/Subsingleton.lean
Modified
MathlibTest/ToDual.lean
Modified
MathlibTest/apply_with.lean
Modified
MathlibTest/toAdditive.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain