Commit 2023-04-20 04:08 8cf71b01

View on Github →

chore: tidy various files (#3530)

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

added theorem LinearMap.mulLeft_toAddMonoidHom

deleted theorem LinearMap.mulLeft_toAddMonoid_hom

added theorem LinearMap.mulRight_toAddMonoidHom

deleted theorem LinearMap.mulRight_toAddMonoid_hom

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Algebra/Pi.lean

Modified Mathlib/Algebra/Algebra/Tower.lean

added theorem AlgEquiv.coe_restrictScalars'

deleted theorem AlgEquiv.coe_restrict_scalars'

added theorem AlgHom.coe_restrictScalars'

deleted theorem AlgHom.coe_restrict_scalars'

added theorem IsScalarTower.coe_toAlgHom'

deleted theorem IsScalarTower.coe_to_alg_hom'

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

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/Analysis/BoxIntegral/Box/Basic.lean

added theorem BoxIntegral.Box.Icc_def

added theorem BoxIntegral.Box.Icc_eq_pi

added theorem BoxIntegral.Box.Ioo_subset_coe

deleted theorem BoxIntegral.Box.bUnion_coe_eq_coe

added theorem BoxIntegral.Box.bunionᵢ_coe_eq_coe

added theorem BoxIntegral.Box.coe_subset_Icc

deleted theorem BoxIntegral.Box.coe_subset_icc

added theorem BoxIntegral.Box.continuousOn_face_Icc

deleted theorem BoxIntegral.Box.continuousOn_face_icc

added theorem BoxIntegral.Box.diam_Icc_le_of_distortion_le

deleted theorem BoxIntegral.Box.diam_icc_le_of_distortion_le

deleted theorem BoxIntegral.Box.icc_def

deleted theorem BoxIntegral.Box.icc_eq_pi

deleted theorem BoxIntegral.Box.ioo_subset_coe

added theorem BoxIntegral.Box.le_iff_Icc

deleted theorem BoxIntegral.Box.le_iff_icc

added theorem BoxIntegral.Box.lower_mem_Icc

deleted theorem BoxIntegral.Box.lower_mem_icc

added theorem BoxIntegral.Box.unionᵢ_Ioo_of_tendsto

deleted theorem BoxIntegral.Box.unionᵢ_ioo_of_tendsto

added theorem BoxIntegral.Box.upper_mem_Icc

deleted theorem BoxIntegral.Box.upper_mem_icc

Modified Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

Modified Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

Modified Mathlib/CategoryTheory/Category/Pairwise.lean

Modified Mathlib/CategoryTheory/Functor/ReflectsIso.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Limits.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

Modified Mathlib/Data/Finmap.lean

Modified Mathlib/Data/LazyList/Basic.lean

modified def LazyList.listEquivLazyList

Modified Mathlib/Data/Matrix/Block.lean

added theorem Matrix.fromBlocks_toBlocks

deleted theorem Matrix.fromBlocks_to_blocks

added theorem Matrix.toBlocks_fromBlocks₁₁

added theorem Matrix.toBlocks_fromBlocks₁₂

added theorem Matrix.toBlocks_fromBlocks₂₁

added theorem Matrix.toBlocks_fromBlocks₂₂

deleted theorem Matrix.to_blocks_from_blocks₁₁

deleted theorem Matrix.to_blocks_from_blocks₁₂

deleted theorem Matrix.to_blocks_from_blocks₂₁

deleted theorem Matrix.to_blocks_from_blocks₂₂

Modified Mathlib/Data/MvPolynomial/Equiv.lean

modified def MvPolynomial.pUnitAlgEquiv

Modified Mathlib/Data/Num/Prime.lean

Modified Mathlib/Data/W/Cardinal.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

modified def AffineMap.weightedVSubOfPoint

Modified Mathlib/LinearAlgebra/FreeModule/Rank.lean

added theorem rank_tensorProduct'

deleted theorem rank_tensor_product'

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/ModelTheory/Syntax.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

Modified Mathlib/Topology/UniformSpace/Compact.lean

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean