Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-23 04:19
19e0ba92
View on Github →
feat: patch for new alias command (
#6172
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Divisibility/Basic.lean
Modified
Mathlib/Algebra/Group/Basic.lean
Modified
Mathlib/Algebra/Group/Defs.lean
Modified
Mathlib/Algebra/GroupPower/Basic.lean
Modified
Mathlib/Algebra/GroupPower/Lemmas.lean
Modified
Mathlib/Algebra/GroupPower/Order.lean
Modified
Mathlib/Algebra/GroupPower/Ring.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Divisibility.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
Modified
Mathlib/Algebra/ModEq.lean
Modified
Mathlib/Algebra/Order/Field/Basic.lean
Modified
Mathlib/Algebra/Order/Field/Power.lean
Modified
Mathlib/Algebra/Order/Group/Defs.lean
Modified
Mathlib/Algebra/Order/Group/MinMax.lean
Modified
Mathlib/Algebra/Order/Group/OrderIso.lean
Modified
Mathlib/Algebra/Order/Kleene.lean
Modified
Mathlib/Algebra/Order/Module.lean
Modified
Mathlib/Algebra/Order/Monoid/Lemmas.lean
Modified
Mathlib/Algebra/Order/Monoid/NatCast.lean
Modified
Mathlib/Algebra/Order/Ring/Defs.lean
Modified
Mathlib/Algebra/Order/Ring/Lemmas.lean
Modified
Mathlib/Algebra/Order/SMul.lean
Modified
Mathlib/Algebra/Order/Sub/Canonical.lean
Modified
Mathlib/Algebra/Order/Sub/Defs.lean
Modified
Mathlib/Algebra/Order/ToIntervalMod.lean
Modified
Mathlib/Algebra/Order/ZeroLEOne.lean
Modified
Mathlib/Algebra/Parity.lean
Modified
Mathlib/Algebra/Ring/Defs.lean
Modified
Mathlib/Algebra/Ring/Divisibility.lean
Modified
Mathlib/Algebra/Star/Basic.lean
Modified
Mathlib/Analysis/Asymptotics/Asymptotics.lean
Modified
Mathlib/Analysis/Asymptotics/Theta.lean
Modified
Mathlib/Analysis/Calculus/ContDiffDef.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/Implicit.lean
Modified
Mathlib/Analysis/Calculus/Inverse.lean
Modified
Mathlib/Analysis/Convex/Basic.lean
Modified
Mathlib/Analysis/Convex/Between.lean
Modified
Mathlib/Analysis/Convex/Function.lean
Modified
Mathlib/Analysis/Convex/Intrinsic.lean
Modified
Mathlib/Analysis/Convex/Side.lean
Modified
Mathlib/Analysis/Convex/Star.lean
Modified
Mathlib/Analysis/Convex/Strict.lean
Modified
Mathlib/Analysis/Convex/Topology.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
Modified
Mathlib/Analysis/LocallyConvex/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/Hom.lean
Modified
Mathlib/Analysis/NormedSpace/Ray.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
Modified
Mathlib/CategoryTheory/Category/Bipointed.lean
Modified
Mathlib/CategoryTheory/Category/Pointed.lean
Modified
Mathlib/CategoryTheory/Category/Preorder.lean
Modified
Mathlib/CategoryTheory/Category/TwoP.lean
Modified
Mathlib/CategoryTheory/CommSq.lean
Modified
Mathlib/CategoryTheory/Functor/FullyFaithful.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
Modified
Mathlib/Data/Array/Basic.lean
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/Finite/Defs.lean
Modified
Mathlib/Data/Finmap.lean
Modified
Mathlib/Data/Finset/Basic.lean
Modified
Mathlib/Data/Finset/Card.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Lattice.lean
Modified
Mathlib/Data/Finset/LocallyFinite.lean
Modified
Mathlib/Data/Finset/Pointwise.lean
Modified
Mathlib/Data/Finset/Slice.lean
Modified
Mathlib/Data/Finset/Sym.lean
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/Fintype/Card.lean
Modified
Mathlib/Data/Int/ModEq.lean
Modified
Mathlib/Data/Int/Order/Units.lean
Modified
Mathlib/Data/Int/Parity.lean
Modified
Mathlib/Data/Int/SuccPred.lean
Modified
Mathlib/Data/Int/Units.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/List/Infix.lean
Modified
Mathlib/Data/List/Nodup.lean
Modified
Mathlib/Data/List/Pairwise.lean
Modified
Mathlib/Data/List/Perm.lean
Modified
Mathlib/Data/List/Sort.lean
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/Multiset/Dedup.lean
Modified
Mathlib/Data/Multiset/LocallyFinite.lean
Modified
Mathlib/Data/Multiset/Powerset.lean
Modified
Mathlib/Data/Nat/Cast/Basic.lean
Modified
Mathlib/Data/Nat/Count.lean
Modified
Mathlib/Data/Nat/Factorial/Basic.lean
Modified
Mathlib/Data/Nat/ModEq.lean
Modified
Mathlib/Data/Nat/Pow.lean
Modified
Mathlib/Data/Nat/Prime.lean
Modified
Mathlib/Data/Nat/SuccPred.lean
Modified
Mathlib/Data/Polynomial/Degree/Definitions.lean
Modified
Mathlib/Data/Rat/NNRat.lean
Modified
Mathlib/Data/Real/ENNReal.lean
Modified
Mathlib/Data/Real/Sqrt.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Set/Countable.lean
Modified
Mathlib/Data/Set/Finite.lean
Modified
Mathlib/Data/Set/Function.lean
Modified
Mathlib/Data/Set/Image.lean
Modified
Mathlib/Data/Set/Lattice.lean
Modified
Mathlib/Data/Set/Pairwise/Basic.lean
Modified
Mathlib/Data/Set/Pointwise/Basic.lean
Modified
Mathlib/Data/Set/Pointwise/Finite.lean
Modified
Mathlib/Data/Set/Prod.lean
Modified
Mathlib/Dynamics/Flow.lean
Modified
Mathlib/Geometry/Euclidean/Triangle.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv.lean
Modified
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
Modified
Mathlib/GroupTheory/FreeGroup.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Subgroup/ZPowers.lean
Modified
Mathlib/Init/Algebra/Functions.lean
Modified
Mathlib/Init/CCLemmas.lean
Modified
Mathlib/Init/Classical.lean
Modified
Mathlib/Init/Data/Int/Order.lean
Modified
Mathlib/Init/Data/List/Lemmas.lean
Modified
Mathlib/Init/Logic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/Basis.lean
Modified
Mathlib/LinearAlgebra/CrossProduct.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
Modified
Mathlib/LinearAlgebra/Ray.lean
Modified
Mathlib/LinearAlgebra/Span.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Equiv/LocalEquiv.lean
Modified
Mathlib/Logic/Function/Iterate.lean
Modified
Mathlib/Logic/Lemmas.lean
Modified
Mathlib/Logic/Pairwise.lean
Modified
Mathlib/Mathport/Syntax.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm.lean
Modified
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace.lean
Modified
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
Modified
Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
Modified
Mathlib/NumberTheory/Bertrand.lean
Modified
Mathlib/Order/Antisymmetrization.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/Basic.lean
Modified
Mathlib/Order/BoundedOrder.lean
Modified
Mathlib/Order/Circular.lean
Modified
Mathlib/Order/CompactlyGenerated.lean
Modified
Mathlib/Order/Compare.lean
Modified
Mathlib/Order/Cover.lean
Modified
Mathlib/Order/Directed.lean
Modified
Mathlib/Order/Disjoint.lean
Modified
Mathlib/Order/Filter/AtTopBot.lean
Modified
Mathlib/Order/Filter/Bases.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/EventuallyConst.lean
Modified
Mathlib/Order/Filter/Extr.lean
Modified
Mathlib/Order/Filter/Germ.lean
Modified
Mathlib/Order/Filter/Lift.lean
Modified
Mathlib/Order/Filter/SmallSets.lean
Modified
Mathlib/Order/Filter/Subsingleton.lean
Modified
Mathlib/Order/Filter/Ultrafilter.lean
Modified
Mathlib/Order/Heyting/Basic.lean
Modified
Mathlib/Order/Irreducible.lean
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/Max.lean
Modified
Mathlib/Order/ModularLattice.lean
Modified
Mathlib/Order/Monotone/Basic.lean
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/RelIso/Basic.lean
Modified
Mathlib/Order/SuccPred/Basic.lean
Modified
Mathlib/Order/SuccPred/Limit.lean
Modified
Mathlib/Order/SupIndep.lean
Modified
Mathlib/Order/Synonym.lean
Modified
Mathlib/Order/UpperLower/Basic.lean
Modified
Mathlib/Order/WithBot.lean
Modified
Mathlib/Probability/IdentDistrib.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent.lean
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
Modified
Mathlib/RingTheory/FiniteType.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/IntegralClosure.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/SetTheory/Cardinal/Basic.lean
Modified
Mathlib/SetTheory/Game/PGame.lean
Modified
Mathlib/SetTheory/Ordinal/Arithmetic.lean
Modified
Mathlib/SetTheory/Surreal/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Ordinal.lean
Modified
Mathlib/Tactic.lean
Deleted
Mathlib/Tactic/Alias.lean
deleted
def
Tactic.Alias.Target.toName
deleted
def
Tactic.Alias.Target.toString
deleted
inductive
Tactic.Alias.Target
deleted
def
Tactic.Alias.aliasIff
deleted
def
Tactic.Alias.appendNamespace
deleted
def
Tactic.Alias.elabAlias
deleted
def
Tactic.Alias.elabAliasLR
deleted
def
Tactic.Alias.elabAliasLRDots
deleted
def
Tactic.Alias.mkIffMpApp
deleted
theorem
alias1
deleted
theorem
alias2
Modified
Mathlib/Tactic/Common.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Module.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
Modified
Mathlib/Topology/Bases.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Bornology/Basic.lean
Modified
Mathlib/Topology/Bornology/Constructions.lean
Modified
Mathlib/Topology/Connected.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/ContinuousOn.lean
Modified
Mathlib/Topology/Inseparable.lean
Modified
Mathlib/Topology/LocalAtTarget.lean
Modified
Mathlib/Topology/LocalHomeomorph.lean
Modified
Mathlib/Topology/MetricSpace/Antilipschitz.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDimension.lean
Modified
Mathlib/Topology/MetricSpace/Holder.lean
Modified
Mathlib/Topology/MetricSpace/Isometry.lean
Modified
Mathlib/Topology/MetricSpace/Lipschitz.lean
Modified
Mathlib/Topology/MetricSpace/MetricSeparated.lean
Modified
Mathlib/Topology/NhdsSet.lean
Modified
Mathlib/Topology/Order/Basic.lean
Modified
Mathlib/Topology/Order/NhdsSet.lean
Modified
Mathlib/Topology/Separation.lean
Modified
Mathlib/Topology/SubsetProperties.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergence.lean
Deleted
test/Alias.lean
deleted
theorem
Alias.A.a_iff_a_and_a
deleted
theorem
Alias.A.ab_iff_ba
deleted
def
Alias.A.bar
deleted
theorem
Alias.A.baz
deleted
theorem
Alias.A.foo
deleted
def
Alias.baz
deleted
theorem
Alias.checkType
deleted
def
Alias.foo