Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-17 14:33
ab56fa28
View on Github →
Revert "chore: revert
#7703
(
#7710
)" This reverts commit f3695eb20c685cfcb5e45f75b1e68a59b8de7efb.
Estimated changes
Modified
Archive/Sensitivity.lean
Modified
Counterexamples/DirectSumIsInternal.lean
Modified
Counterexamples/Pseudoelement.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Modified
Mathlib/Algebra/Category/AlgebraCat/Basic.lean
Modified
Mathlib/Algebra/Category/AlgebraCat/Limits.lean
Modified
Mathlib/Algebra/Category/GroupCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/GroupCat/Basic.lean
Modified
Mathlib/Algebra/Category/GroupCat/Biproducts.lean
Modified
Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean
Modified
Mathlib/Algebra/Category/GroupCat/Injective.lean
Modified
Mathlib/Algebra/Category/GroupCat/Limits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Biproducts.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Colimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Kernels.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Projective.lean
Modified
Mathlib/Algebra/Category/MonCat/Basic.lean
Modified
Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/Ring/Colimits.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/DirectSum/Ring.lean
Modified
Mathlib/Algebra/Homology/ModuleCat.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/Lie/DirectSum.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
modified
theorem
LieModuleEquiv.ofTop_apply
Modified
Mathlib/Algebra/Lie/UniversalEnveloping.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
Modified
Mathlib/AlgebraicGeometry/AffineScheme.lean
Modified
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/Spec.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/CechNerve.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory.lean
Modified
Mathlib/AlgebraicTopology/TopologicalSimplex.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
deleted
theorem
IsSelfAdjoint.isClosed
deleted
theorem
LinearPMap.adjoint_graph_eq_graph_adjoint
deleted
theorem
LinearPMap.adjoint_isClosed
deleted
theorem
LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint
deleted
def
Submodule.adjoint
deleted
theorem
Submodule.mem_adjoint_iff
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean
Modified
Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
Modified
Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
Modified
Mathlib/CategoryTheory/Adjunction/Comma.lean
Modified
Mathlib/CategoryTheory/Adjunction/Evaluation.lean
Modified
Mathlib/CategoryTheory/Adjunction/Lifting.lean
Modified
Mathlib/CategoryTheory/Closed/Cartesian.lean
Modified
Mathlib/CategoryTheory/Closed/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Closed/Monoidal.lean
Modified
Mathlib/CategoryTheory/Limits/HasLimits.lean
Modified
Mathlib/CategoryTheory/Limits/KanExtension.lean
Modified
Mathlib/CategoryTheory/Limits/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Presheaf.lean
Modified
Mathlib/CategoryTheory/Monad/Algebra.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
Modified
Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Adjunction.lean
Modified
Mathlib/CategoryTheory/Sites/Sheaf.lean
Modified
Mathlib/CategoryTheory/Subobject/Comma.lean
Modified
Mathlib/CategoryTheory/Yoneda.lean
Modified
Mathlib/Combinatorics/Quiver/Covering.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Control/Fold.lean
Modified
Mathlib/Data/Matrix/Reflection.lean
Modified
Mathlib/Data/MvPolynomial/Rename.lean
Modified
Mathlib/FieldTheory/AbelRuffini.lean
Modified
Mathlib/FieldTheory/Adjoin.lean
Modified
Mathlib/FieldTheory/IntermediateField.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/SplittingField/Construction.lean
Modified
Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
Modified
Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Sign.lean
Modified
Mathlib/Lean/Expr/Basic.lean
deleted
def
Lean.ConstantInfo.getUsedConstants
deleted
def
Lean.Expr.getUsedConstants'
deleted
def
Lean.NameSet.append
Modified
Mathlib/LinearAlgebra/AffineSpace/Independent.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
Modified
Mathlib/LinearAlgebra/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Finrank.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Norm.lean
Modified
Mathlib/LinearAlgebra/Isomorphisms.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct.lean
Modified
Mathlib/LinearAlgebra/Prod.lean
deleted
theorem
LinearEquiv.skewSwap_apply
deleted
theorem
LinearEquiv.skewSwap_symm_apply
Modified
Mathlib/ModelTheory/DirectLimit.lean
Modified
Mathlib/ModelTheory/Fraisse.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/Order/Category/PartOrd.lean
Modified
Mathlib/Order/InitialSeg.lean
Modified
Mathlib/Order/LocallyFinite.lean
Modified
Mathlib/RepresentationTheory/Action.lean
Modified
Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
Modified
Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
Modified
Mathlib/RepresentationTheory/Rep.lean
Modified
Mathlib/RingTheory/ClassGroup.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
Modified
Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
Modified
Mathlib/RingTheory/Etale.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Ideal/QuotientOperations.lean
Modified
Mathlib/RingTheory/Kaehler.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/Norm.lean
Modified
Mathlib/RingTheory/PowerSeries/Basic.lean
Modified
Mathlib/RingTheory/SimpleModule.lean
Modified
Mathlib/RingTheory/Subring/Basic.lean
Modified
Mathlib/RingTheory/Subsemiring/Basic.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/Topology/Category/CompHaus/Projective.lean
Modified
Mathlib/Topology/Category/Profinite/Basic.lean
Modified
Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
Modified
Mathlib/Topology/Category/Profinite/Projective.lean
Modified
Mathlib/Topology/Category/Stonean/Limits.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
Modified
Mathlib/Topology/ContinuousFunction/Compact.lean
Modified
Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Instances/Complex.lean
Modified
lake-manifest.json
Modified
lean-toolchain