Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-09-29 06:57
d3263b23
View on Github →
chore: exactly 4 spaces in theorems (
#7328
)
Estimated changes
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Group/Defs.lean
Modified
Mathlib/Algebra/Group/Ext.lean
Modified
Mathlib/Algebra/Group/Pi.lean
Modified
Mathlib/Algebra/GroupPower/Lemmas.lean
Modified
Mathlib/Algebra/Hom/Equiv/Basic.lean
Modified
Mathlib/Algebra/Hom/Equiv/Units/Basic.lean
Modified
Mathlib/Algebra/Hom/Group/Basic.lean
Modified
Mathlib/Algebra/Hom/Group/Defs.lean
Modified
Mathlib/Algebra/Hom/GroupAction.lean
Modified
Mathlib/Algebra/Hom/Units.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
Modified
Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject.lean
Modified
Mathlib/Analysis/Convex/Combination.lean
Modified
Mathlib/Analysis/NormedSpace/WeakDual.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/Basic.lean
modified
theorem
CategoryTheory.Functor.map_comp_assoc
Modified
Mathlib/CategoryTheory/Limits/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
Modified
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
Modified
Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
Modified
Mathlib/CategoryTheory/Subobject/MonoOver.lean
Modified
Mathlib/CategoryTheory/Triangulated/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Triangulated.lean
Modified
Mathlib/CategoryTheory/Types.lean
Modified
Mathlib/Combinatorics/Quiver/Path.lean
Modified
Mathlib/Combinatorics/SetFamily/Compression/UV.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
Modified
Mathlib/Computability/TMToPartrec.lean
Modified
Mathlib/Control/Fold.lean
Modified
Mathlib/Control/Functor/Multivariate.lean
Modified
Mathlib/Data/Analysis/Topology.lean
modified
theorem
locallyFinite_iff_exists_realizer
Modified
Mathlib/Data/Array/Defs.lean
Modified
Mathlib/Data/ByteArray.lean
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Int/GCD.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/List/Chain.lean
Modified
Mathlib/Data/List/Defs.lean
Modified
Mathlib/Data/Nat/Cast/Field.lean
Modified
Mathlib/Data/Nat/Fib.lean
Modified
Mathlib/Data/Option/Basic.lean
Modified
Mathlib/Data/PFunctor/Multivariate/M.lean
Modified
Mathlib/Data/PFunctor/Univariate/M.lean
Modified
Mathlib/Data/Polynomial/FieldDivision.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/Real/Sqrt.lean
Modified
Mathlib/Data/Seq/Computation.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Sigma/Basic.lean
Modified
Mathlib/Data/Sigma/Lex.lean
Modified
Mathlib/Data/Sign.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Data/Sym/Sym2.lean
Modified
Mathlib/Data/TypeVec.lean
Modified
Mathlib/Data/UnionFind.lean
modified
theorem
UFModel.Agrees.mk'
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/Vector/MapLemmas.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/Subfield.lean
Modified
Mathlib/Geometry/Manifold/ChartedSpace.lean
Modified
Mathlib/Geometry/Manifold/Complex.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/SchurZassenhaus.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/Lean/Meta/Simp.lean
Modified
Mathlib/LinearAlgebra/Lagrange.lean
Modified
Mathlib/LinearAlgebra/Orientation.lean
Modified
Mathlib/LinearAlgebra/Prod.lean
modified
def
Submodule.sndEquiv
Modified
Mathlib/Logic/Function/Basic.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/MeasureTheory/Measure/Complex.lean
Modified
Mathlib/MeasureTheory/Measure/OuterMeasure.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/Hom/Set.lean
modified
def
OrderIso.Set.univ
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/MinMax.lean
Modified
Mathlib/Order/SuccPred/Basic.lean
Modified
Mathlib/RingTheory/EisensteinCriterion.lean
Modified
Mathlib/RingTheory/FreeCommRing.lean
Modified
Mathlib/RingTheory/IntegralClosure.lean
Modified
Mathlib/RingTheory/IntegralDomain.lean
Modified
Mathlib/RingTheory/Nilpotent.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
Modified
Mathlib/Tactic/Abel.lean
Modified
Mathlib/Tactic/Have.lean
Modified
Mathlib/Tactic/Linarith/Datatypes.lean
Modified
Mathlib/Tactic/Linarith/Parsing.lean
Modified
Mathlib/Tactic/MkIffOfInductiveProp.lean
Modified
Mathlib/Tactic/NormNum/Pow.lean
Modified
Mathlib/Tactic/NormNum/Prime.lean
Modified
Mathlib/Tactic/PrintPrefix.lean
Modified
Mathlib/Tactic/Relation/Trans.lean
Modified
Mathlib/Tactic/Sat/FromLRAT.lean
Modified
Mathlib/Tactic/SimpRw.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/ToAdditive.lean
modified
def
ToAdditive.updateDecl
Modified
Mathlib/Tactic/TryThis.lean
Modified
Mathlib/Tactic/Zify.lean
Modified
Mathlib/Topology/AlexandrovDiscrete.lean
Modified
Mathlib/Topology/Algebra/Order/Archimedean.lean
Modified
Mathlib/Topology/Bases.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Connected.lean
Modified
Mathlib/Topology/EMetricSpace/Basic.lean
Modified
Mathlib/Topology/PathConnected.lean
Modified
Mathlib/Topology/Sheaves/Presheaf.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean