Sync upstream mathlib4 (2026-05-11, +11 commits)#3
Merged
Conversation
…ebra norm equals the square root of the spectral radius of star a * a (#33178) Adds lemmas that the ||a||^2_A=sqrt(spectralRadius C (star a * a)). I think it would be helpful to have these lemmas available in Mathlib. It'll help with some of the other things I'm working on. Feel free to move them to a different file or rename them as you see fit. Co-authored-by: Gregory Wickham <gwickham99@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
If `f : ℂ → ℂ` is meromorphic, establish the circle integrability of the function `a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` and compute values of the circle integral. The circle integral in question is one of the main terms in Cartan's classic formula, describing the characteristic function `characteristic f ⊤ r` as a sum of circle averages. This is the second section of a four-part PR, establishing Cartan's formula and its most immediate corollaries.
…ctions (#38984) Add simple, but useful, variants of the principle of isolated zeros for meromorphic functions.
Plus a small golf.
…tive subobjects (#36553)
…(#36891) Used in the CGT repo. Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
…n lemmas (#38962) This PR renames the companion lemmas of `Submodule.subtypeL` for consistency with `Submodule.mkQL` (introduced in PR #38811). Specifically, `Submodule.coe_subtypeL` is renamed to `Submodule.toLinearMap_subtypeL` (to accurately reflect that it projects to the underlying LinearMap, not a function-level coercion), and `Submodule.coe_subtypeL'` is renamed to `Submodule.coe_subtypeL` (since this is the genuine function-level coercion lemma).
…sional (#38579) `Submodule.ClosedComplemented.of_quotient_finiteDimensional` currently says that any finite codimension *closed* subspace of a Banach space is topologically complemented. The current proof uses the Banach open mapping theorem. In fact the result holds for any TVS over a nontrivially normed field, and we have the stronger result that any algebraic complement of a finite codimension closed subspace is in fact a topological complement.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
8 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Automated daily sync from
leanprover-community/mathlib4@master.50f0559af90cecbf1ed7cf4459565c7168329903Auto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Medium Risk
Medium risk due to wide-ranging library changes across algebra/topology/set theory (new lemmas, moved definitions, and import reshuffles) that may affect downstream proofs via typeclass/rewriter behavior, though changes are largely additive and refactoring-focused.
Overview
Syncs 11 upstream commits.
Adds a new complex analysis file
Analysis/Complex/ValueDistribution/Cartan(and imports it fromMathlib.lean) establishing circle-integrability/average results forlog ‖meromorphicTrailingCoeffAt (f · - a) 0‖as groundwork for Cartan’s formula.Extends “directed supremum preserves commutativity” support by adding
isMulCommutative_iSuplemmas/instances forSubsemigroup,Submonoid,Subgroup,Subsemiring/Subring, and (non-unital, star)Subalgebravariants, plus related directedStarSubalgebracoercion lemmas.Refactors/extends meromorphic infrastructure with new
fun-form iff lemmas for add/sub meromorphicity, order/trailing-coefficient negation lemmas, and additional trailing-coefficient arithmetic lemmas; also tweaksExpectpositivity/strictness lemmas and adds C⋆-algebra spectral-radius-to-real/norm-squared identities.Includes several topology/linear-algebra maintenance changes: moves
Submodule.subtypeLinto theSubmodulenamespace with deprecations, relocates closed-complemented results toTopology/Algebra/Module/FiniteDimension, and simplifies some proofs/simpusage; plus newcodiscreteWithinlemmas for complements of singleton/finite sets and new ordinal/cardinal lemmas aroundω^2bounds, cofinalities, and inaccessibles.Reviewed by Cursor Bugbot for commit 5c2406f. Bugbot is set up for automated code reviews on this repo. Configure here.