Commit 2024-08-07 07:08 cfba2471

View on Github →

chore: backports for leanprover/lean4#4814 (part 21) (#15510)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Rank.lean

Modified Mathlib/Algebra/Category/Grp/Injective.lean

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

modified theorem NonUnitalStarAlgebra.span_eq_toSubmodule

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

modified theorem cfc_const_one

modified theorem cfc_eq_cfc_iff_eqOn

modified theorem cfc_id'

modified theorem cfc_id

modified theorem cfc_map_spectrum

modified theorem cfc_one

modified theorem cfc_star_id

Modified Mathlib/Analysis/CStarAlgebra/Unitization.lean

Modified Mathlib/Analysis/Normed/Algebra/Unitization.lean

modified theorem Unitization.uniformEmbedding_addEquiv

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

modified theorem CategoryTheory.Equivalence.precoherent

modified theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff

modified theorem CategoryTheory.Equivalence.preregular

modified theorem CategoryTheory.Equivalence.preregular_isSheaf_iff

modified def CategoryTheory.Equivalence.sheafCongrPrecoherent

modified def CategoryTheory.Equivalence.sheafCongrPreregular

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

modified theorem Subalgebra.eq_of_le_of_finrank_eq

modified theorem Subalgebra.eq_of_le_of_finrank_le

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

modified theorem AdicCompletion.map_ext

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

modified def FractionalIdeal.adjoinIntegral

modified theorem FractionalIdeal.adjoinIntegral_coe

modified theorem FractionalIdeal.isFractional_adjoin_integral

modified theorem FractionalIdeal.isFractional_of_fg

modified theorem FractionalIdeal.mem_adjoinIntegral_self

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Real.lean

modified theorem summable_prod_of_nonneg

modified theorem summable_sigma_of_nonneg

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

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

Modified Mathlib/Topology/ContinuousFunction/CompactlySupported.lean

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

modified theorem ContinuousMapZero.toContinuousMap_injective

Modified Mathlib/Topology/Instances/AddCircle.lean

modified theorem AddCircle.continuousAt_equivIco

modified theorem AddCircle.continuousAt_equivIoc

modified def AddCircle.homeoIccQuot

modified theorem continuousAt_toIcoMod

modified theorem continuousAt_toIocMod

modified theorem toIcoMod_eventuallyEq_toIocMod

Modified Mathlib/Topology/Instances/ENNReal.lean

modified theorem cauchySeq_of_edist_le_of_summable

Modified Mathlib/Topology/MetricSpace/Gluing.lean

modified def Metric.glueMetricApprox