Skip to content

Import several complex variables, analytic germs, and extension theory #490

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 23 commits into
base: main
Choose a base branch
from
Open

Import several complex variables, analytic germs, and extension theory #490

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
cf826f6
Import Classical several complex variables
Vilin97 Sep 21, 2026
33d3176
Port full several complex variables library and clear scoped checks
Vilin97 Sep 21, 2026
cf7b403
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 22, 2026
6ca2ccf
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 23, 2026
425f292
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 23, 2026
0743324
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 24, 2026
6716617
Migrate SeveralComplexVariables to explicit public Lean modules
Vilin97 Sep 25, 2026
2e5943c
Merge remote-tracking branch 'origin/main' into codex/import42-lean-scv
Vilin97 Sep 25, 2026
e61bd41
Merge remote-tracking branch 'origin/main' into codex/import42-lean-scv
Vilin97 Sep 25, 2026
6d3a147
Align SCV claims, source references, and overlap documentation
Vilin97 Sep 25, 2026
c5b0808
Merge remote-tracking branch 'origin/main' into HEAD
Vilin97 Sep 25, 2026
07ef38d
Wrap SCV references and keep generated card concise
Vilin97 Sep 25, 2026
a3b27d5
Merge main attribution updates into SCV import
Vilin97 Sep 25, 2026
a42cfa1
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
6adc7eb
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
48b33da
Merge remote-tracking branch 'origin/main' into HEAD
Vilin97 Sep 26, 2026
5700b5e
Merge current main without changing project claims or gates
Vilin97 Sep 26, 2026
02c40ce
Merge current main without changing project claims or gates
Vilin97 Sep 26, 2026
0cdc1a8
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 26, 2026
719fd8b
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 26, 2026
d36bb1c
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 26, 2026
57033c0
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 26, 2026
a472b2c
Merge remote-tracking branch 'origin/main' into pr-490
github-actions[bot] Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
163 changes: 163 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7598,6 +7598,169 @@ public import LeanPool.SetTheory.Realize
public import LeanPool.SetTheory.RealizeBuilders
public import LeanPool.SetTheory.RealizeCore
public import LeanPool.SetTheory.SimpAttr
public import LeanPool.SeveralComplexVariables
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analysis
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analysis.Connected
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analysis.LinearFunctional
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analysis.OpenMapping
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analysis.TaylorBounds
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.CoefficientPolynomial
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.CoordinateChange
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Elimination
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Factorization
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Fiber
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.IntrinsicOrder
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Noetherian
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Order
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Polynomial
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.RelativePrimality
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Units
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticGerm.Weierstrass
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Codimension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.CoordinatePlane
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.FunctionSpace
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Hartogs
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Holomorphic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Regular
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.AnalyticSet.Removable
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Analyticity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.BallAutomorphisms
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Biholomorphic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.BiholomorphicRigidity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CartanThullen
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CartanUniqueness
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyCoefficients
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyDerivatives
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyEstimates
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyIntegral
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyPompeiu
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyRiemann
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchySeries
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CauchyTransform
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Circular
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CircularContinuation
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CommonExtension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.CompactHole
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ContourIntegral
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Derivatives
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.DomainOfHolomorphy
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.DominatedIntegral
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.FunctionSpace
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.FunctionSpace.Extension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HartogsContinuation
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HartogsDomain
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HartogsExtension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HartogsLaurent
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HartogsSeries
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity.BoundaryDistance
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity.Exhaustion
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity.Hull
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity.Thullen
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicConvexity.Transport
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.HolomorphicLp
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.IdentityPrinciple
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ImplicitGraph
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ImplicitMapping
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.InjectiveMapping
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.InjectiveMapping.CorankOne
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.InjectiveMapping.CriticalSet
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.InjectiveMapping.Immersion
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.InjectiveMapping.OneVariable
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Integral
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Integral.Circle
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.IsolatedSingularity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentApproximation
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Annulus
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Coefficients
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Convergence
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Iterated
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Neighborhoods
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.OneVariable
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.ProductCoefficients
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.ProductExpansion
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LaurentSeries.Uniqueness
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviConvexity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviConvexity.Independence
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviConvexity.Invariance
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviConvexity.Necessity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviConvexity.Peak
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviForm
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LeviForm.Holomorphic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LocallyBounded
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.LocallyUniform
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.MaximumModulus
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Montel
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Osgood
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ParametricIntegral
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Plurisubharmonic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Polydisc
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PolydiscMeanValue
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PolydiscTaylor
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Polynomial
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Polynomial.OfFn
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PolynomialDerivatives
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PowerSeriesConvergence
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PowerSeriesConvergence.Analytic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.PowerSeriesConvergence.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Pseudoconvexity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RealUniqueness
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reindex
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.Extension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.GeometricConvexity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.HolomorphicConvexity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.Hull
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.MonomialSeparation
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Reinhardt.PartialHull
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.Cauchy
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.ExceptionalSet
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.Geometry
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.Gluing
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.Local
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.RemovableSingularity.OneVariable
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Runge
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Runge.Examples
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic.Baire
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic.FiberExtension
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic.HartogsLemma
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic.MeanValue
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SeparateAnalytic.Submean
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.SphericalShell
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Subharmonic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Subharmonic.Majorant
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Subharmonic.SmoothCriterion
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology.CompactExhaustion
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology.Frontier
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology.Graph
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology.Path
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.Topology.UpperSemicontinuous
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain.Bochner
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain.Disc
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain.Gluing
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.TubeDomain.StarConvex
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.WeierstrassDivision
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.WeierstrassDivision.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.WeierstrassDivision.CoordinatePower
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.WeierstrassDivision.Picard
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.WeierstrassPreparation
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ZeroSets
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ZeroSets.Basic
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ZeroSets.Connected
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ZeroSets.Local
public import LeanPool.SeveralComplexVariables.SeveralComplexVariables.ZeroSets.Persistence
public import LeanPool.SeveralComplexVariables.Solution
public import LeanPool.Shannon1948Formalization
public import LeanPool.Shannon1948Formalization.Entropy
public import LeanPool.Shannon1948Formalization.Entropy.Approx
Expand Down
Loading
Loading