Commit 2024-08-07 07:08 06423177

View on Github →

chore: backports for leanprover/lean4#4814 (part 22) (#15511)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean

modified theorem PresheafOfModules.isSheaf_of_isLimit

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

Modified Mathlib/Analysis/Convex/Radon.lean

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

modified theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm

modified theorem Matrix.fromBlocks_mul_fromRows

modified theorem Matrix.fromColumns_mulVec_sum_elim

modified theorem Matrix.fromColumns_mul_fromBlocks

modified theorem Matrix.fromColumns_mul_fromRows

modified theorem Matrix.fromColumns_mul_fromRows_eq_one_comm

modified theorem Matrix.fromRows_mul

modified theorem Matrix.fromRows_mulVec

modified theorem Matrix.fromRows_mul_fromColumns

modified theorem Matrix.mul_fromColumns

modified theorem Matrix.sum_elim_vecMul_fromRows

modified theorem Matrix.vecMul_fromColumns

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

modified theorem Matrix.mulVec_surjective_iff_exists_right_inverse

modified theorem Matrix.vecMul_surjective_iff_exists_left_inverse

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

modified theorem QuadraticMap.PosDef.add

Modified Mathlib/RepresentationTheory/Maschke.lean

modified theorem LinearMap.conjugate_i

modified theorem LinearMap.equivariantProjection_condition

Modified Mathlib/RingTheory/SimpleModule.lean

modified theorem IsSemisimpleModule.congr

modified theorem LinearMap.isSemisimpleModule_iff_of_bijective

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified theorem Algebra.TensorProduct.congr_trans

modified theorem Algebra.TensorProduct.map_comp

Modified Mathlib/Topology/MetricSpace/Perfect.lean

modified theorem Perfect.exists_nat_bool_injection

modified theorem Perfect.small_diam_splitting

Modified Mathlib/Topology/TietzeExtension.lean

modified theorem ContinuousMap.exists_extension'

modified theorem ContinuousMap.exists_extension

modified theorem ContinuousMap.exists_extension_forall_mem

modified theorem ContinuousMap.exists_forall_mem_restrict_eq

modified theorem ContinuousMap.exists_restrict_eq