Commit 2024-08-05 03:02 39adedf1

View on Github →

chore: backports for leanprover/lean4#4814 (part 16) (#15427) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

Modified Mathlib/Algebra/Algebra/Unitization.lean

modified theorem Unitization.starLift_symm_apply_apply

Modified Mathlib/Algebra/DirectSum/Internal.lean

modified theorem Submodule.setLike.coe_galgebra_toFun

Modified Mathlib/Algebra/DirectSum/Module.lean

modified theorem DirectSum.linearEquivFunOnFintype_lof

modified theorem DirectSum.linearEquivFunOnFintype_symm_single

Modified Mathlib/Algebra/Homology/Embedding/TruncGE.lean

Modified Mathlib/Algebra/Homology/HomotopyCofiber.lean

modified theorem HomologicalComplex.homotopyCofiber.descSigma_ext_iff

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified theorem AddMonoidAlgebra.of'_commute

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

modified theorem AddMonoidAlgebra.apply_add_of_supDegree_le

modified theorem AddMonoidAlgebra.le_infDegree_mul

modified theorem AddMonoidAlgebra.supDegree_mul_le

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

modified theorem MvPolynomial.eval_eval₂

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

Modified Mathlib/Analysis/Convex/Mul.lean

modified theorem ConcaveOn.smul'

modified theorem ConcaveOn.smul_convexOn

modified theorem ConvexOn.smul''

modified theorem ConvexOn.smul_concaveOn'

Modified Mathlib/CategoryTheory/Abelian/LeftDerived.lean

modified theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality

modified theorem CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'

Modified Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean

Modified Mathlib/CategoryTheory/Abelian/RightDerived.lean

modified theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles

modified theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

modified theorem CategoryTheory.PreGaloisCategory.comp_autMap_apply

Modified Mathlib/CategoryTheory/Localization/Triangulated.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

modified theorem SimpleGraph.incMatrix_mul_transpose_diag

modified theorem SimpleGraph.sum_incMatrix_apply

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

modified theorem SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

modified theorem SimpleGraph.IsSRGWith.param_eq

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

modified theorem SimpleGraph.IsTuranMaximal.card_parts

modified theorem SimpleGraph.IsTuranMaximal.card_parts_le

modified theorem SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card

modified theorem SimpleGraph.IsTuranMaximal.isEquipartition

modified theorem SimpleGraph.IsTuranMaximal.iso

modified theorem SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

modified theorem CompleteLattice.Independent.linearIndependent

modified theorem CompleteLattice.independent_iff_linearIndependent_of_ne_zero

modified theorem DFinsupp.coprodMap_apply

Modified Mathlib/LinearAlgebra/Finsupp.lean

modified theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply

modified theorem Submodule.mulLeftMap_eq_mulRightMap_of_commute

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

modified theorem Matrix.conjTranspose_mul_self_eq_zero

modified theorem Matrix.conjTranspose_mul_self_mul_eq_zero

modified theorem Matrix.mul_conjTranspose_mul_self_eq_zero

modified theorem Matrix.mul_self_mul_conjTranspose_eq_zero

modified theorem Matrix.self_mul_conjTranspose_eq_zero

modified theorem Matrix.self_mul_conjTranspose_mul_eq_zero

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/QuotientPi.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

modified theorem MulChar.coe_toMonoidHom

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

modified theorem HahnModule.of_symm_smul

Modified Mathlib/RingTheory/Valuation/Integers.lean

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem IsCompact.mem_nhdsSet_prod_of_forall

modified theorem IsCompact.mem_prod_nhdsSet_of_forall

modified theorem IsCompact.nhdsSet_prod_eq_biSup

modified theorem IsCompact.prod_nhdsSet_eq_biSup

modified theorem IsCompact.tendsto_nhds_of_unique_mapClusterPt

modified theorem tendsto_nhds_of_unique_mapClusterPt

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/DenseEmbedding.lean

modified theorem DenseEmbedding.dense_image

modified theorem DenseEmbedding.inj_iff

modified theorem DenseEmbedding.to_embedding

modified theorem DenseInducing.closure_range

modified theorem DenseInducing.extend_eq

modified theorem DenseInducing.extend_eq_at'

modified theorem DenseInducing.extend_eq_at

modified theorem DenseInducing.extend_eq_of_tendsto

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/Order/ProjIcc.lean

Modified Mathlib/Topology/Separation.lean

modified theorem Filter.Tendsto.eventually_ne

modified theorem t1Space_antitone

Modified Mathlib/Topology/ShrinkingLemma.lean

modified theorem ShrinkingLemma.PartialRefinement.exists_gt

Modified Mathlib/Topology/UniformSpace/Separation.lean

modified theorem Filter.Tendsto.inseparable_iff_uniformity