Commit 2024-08-08 02:10 f786e149

View on Github →

chore: backports for leanprover/lean4#4814 (part 32) (#15577)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

modified theorem NonUnitalAlgHom.map_adjoin

modified theorem NonUnitalAlgHom.map_adjoin_singleton

modified theorem NonUnitalAlgebra.comap_top

modified theorem NonUnitalAlgebra.map_bot

modified theorem NonUnitalAlgebra.map_sup

modified theorem NonUnitalAlgebra.range_top_iff_surjective

Modified Mathlib/Algebra/DirectLimit.lean

modified def AddCommGroup.DirectLimit

modified def Module.DirectLimit

Modified Mathlib/Algebra/DirectSum/Module.lean

modified theorem DirectSum.component.lof_self

modified theorem DirectSum.component.of

modified theorem DirectSum.lof_apply

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Lie/Rank.lean

modified theorem LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero

modified theorem LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank

modified theorem LieAlgebra.polyCharpoly_coeff_rank_ne_zero

modified theorem LieAlgebra.rank_eq_natTrailingDegree

modified theorem LieAlgebra.rank_le_card

modified theorem LieAlgebra.rank_le_finrank

modified theorem LieAlgebra.rank_le_natTrailingDegree_charpoly_ad

modified theorem LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero

modified theorem LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank

modified theorem LieModule.polyCharpoly_coeff_rank_ne_zero

modified theorem LieModule.rank_eq_natTrailingDegree

modified theorem LieModule.rank_le_card

modified theorem LieModule.rank_le_finrank

modified theorem LieModule.rank_le_natTrailingDegree_charpoly_ad

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

modified theorem BoxIntegral.IntegrationParams.MemBaseSet.mono'

modified theorem BoxIntegral.IntegrationParams.MemBaseSet.mono

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

modified theorem CategoryTheory.Functor.homologySequenceδ_naturality

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

modified theorem contMDiffAt_iff_contMDiffAt_nhds

modified theorem contMDiffAt_iff_contMDiffOn_nhds

modified theorem contMDiffAt_iff_source_of_mem_source

modified theorem contMDiffAt_iff_target_of_mem_source

modified theorem contMDiffOn_iff_source_of_mem_maximalAtlas

modified theorem contMDiffWithinAt_iff_contMDiffOn_nhds

modified theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas

modified theorem contMDiffWithinAt_iff_source_of_mem_source

modified theorem contMDiffWithinAt_iff_target_of_mem_source

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

modified theorem TensorProduct.gradedComm_algebraMap

modified theorem TensorProduct.gradedComm_algebraMap_tmul

modified theorem TensorProduct.gradedComm_one

modified theorem TensorProduct.gradedComm_one_tmul

modified theorem TensorProduct.gradedComm_tmul_algebraMap

modified theorem TensorProduct.gradedComm_tmul_one

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/RingTheory/Generators.lean

modified theorem Algebra.Generators.Hom.comp_id

modified theorem Algebra.Generators.Hom.id_comp

modified theorem Algebra.Generators.Hom.toAlgHom_comp_apply

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean