OAI/Geometry/KahlerSplitting/Model.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniversalCoverSplitting.Model line 15

   Also declared: ComparatorChallenges/KahlerSplitting.lean:14 (same declaration text).

2. abbrev OAI.UniversalCoverSplitting.model line 16

   Also declared: ComparatorChallenges/KahlerSplitting.lean:15 (same declaration text).

3. structure OAI.UniversalCoverSplitting.ComplexManifold line 18

   Also declared: ComparatorChallenges/KahlerSplitting.lean:17 (same declaration text).

4. abbrev OAI.UniversalCoverSplitting.Tangent line 31

   Also declared: ComparatorChallenges/KahlerSplitting.lean:30 (same declaration text).

5. abbrev OAI.UniversalCoverSplitting.RealMetricField line 32

   Also declared: ComparatorChallenges/KahlerSplitting.lean:31 (same declaration text).

6. def OAI.UniversalCoverSplitting.metricInChart line 35

   Also declared: ComparatorChallenges/KahlerSplitting.lean:34 (same declaration text).

7. def OAI.UniversalCoverSplitting.fundamentalInChart line 41

   Also declared: ComparatorChallenges/KahlerSplitting.lean:40 (same declaration text).

8. structure OAI.UniversalCoverSplitting.KahlerMetric line 45

   Also declared: ComparatorChallenges/KahlerSplitting.lean:44 (same declaration text).

9. abbrev OAI.UniversalCoverSplitting.ProjectionField line 57

   Also declared: ComparatorChallenges/KahlerSplitting.lean:56 (same declaration text).

10. def OAI.UniversalCoverSplitting.projectionInChart line 60

    Also declared: ComparatorChallenges/KahlerSplitting.lean:59 (same declaration text).

11. def OAI.UniversalCoverSplitting.HolomorphicProjection line 66

    Also declared: ComparatorChallenges/KahlerSplitting.lean:65 (same declaration text).

12. def OAI.UniversalCoverSplitting.Integrable line 69

    Also declared: ComparatorChallenges/KahlerSplitting.lean:68 (same declaration text).

13. structure OAI.UniversalCoverSplitting.HolomorphicSplitting line 78

    Also declared: ComparatorChallenges/KahlerSplitting.lean:77 (same declaration text).

14. def OAI.UniversalCoverSplitting.complementaryProjection line 85

    Also declared: ComparatorChallenges/KahlerSplitting.lean:84 (same declaration text).

15. def OAI.UniversalCoverSplitting.LocalBiholomorphism line 89

    Also declared: ComparatorChallenges/KahlerSplitting.lean:88 (same declaration text).

16. structure OAI.UniversalCoverSplitting.OrdinaryUniversalCover line 96

    Also declared: ComparatorChallenges/KahlerSplitting.lean:95 (same declaration text).

17. def OAI.UniversalCoverSplitting.CompatibleProduct line 104

    Distinct definitions of this name: ComparatorChallenges/KahlerSplitting.lean:103 (same statement text; different proof or body). Qualify references as OAI.UniversalCoverSplitting.CompatibleProduct@path.