Documentation

LeanPool.HopfProblem.Prelude

Imports

Init
Mathlib.CategoryTheory.ExtremalEpi
Mathlib.Dynamics.OmegaLimit
Mathlib.GroupTheory.PresentedGroup
Mathlib.GroupTheory.PushoutI
Mathlib.GroupTheory.SemidirectProduct
Mathlib.Order.CompletePartialOrder
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.PicardGroup
Mathlib.RingTheory.TotallySplit
Mathlib.Tactic.Abel
Mathlib.Tactic.Choose
Mathlib.Tactic.Continuity
Mathlib.Tactic.Convert
Mathlib.Tactic.Ext
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FinCases
Mathlib.Tactic.FunProp
Mathlib.Tactic.GCongr
Mathlib.Tactic.Generalize
Mathlib.Tactic.Group
Mathlib.Tactic.IntervalCases
Mathlib.Tactic.Lift
Mathlib.Tactic.Linarith
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.NormNum
Mathlib.Tactic.Positivity
Mathlib.Tactic.Ring
Mathlib.Tactic.SplitIfs
Mathlib.Tactic.Tauto
Mathlib.Tactic.WLOG
Mathlib.Topology.Gluing
Mathlib.Topology.Subpath
Mathlib.Algebra.AffineMonoid.Basic
Mathlib.Algebra.Homology.ConcreteCategory
Mathlib.Algebra.Homology.GrothendieckAbelian
Mathlib.Algebra.Homology.HomologicalComplexBiprod
Mathlib.Algebra.Homology.HomologySequenceLemmas
Mathlib.Algebra.Ring.IsFormallyReal
Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
Mathlib.Analysis.Calculus.ImplicitContDiff
Mathlib.Analysis.Calculus.TaylorIntegral
Mathlib.Analysis.Complex.BranchLogRoot
Mathlib.Analysis.Complex.Conformal
Mathlib.Analysis.Complex.HasPrimitives
Mathlib.Analysis.Complex.OpenMapping
Mathlib.Analysis.Complex.Schwarz
Mathlib.Analysis.Convex.GaugeRescale
Mathlib.Analysis.InnerProductSpace.OfNorm
Mathlib.Analysis.SpecialFunctions.Artanh
Mathlib.CategoryTheory.EffectiveEpi.Comp
Mathlib.Combinatorics.Quiver.ReflQuiver
Mathlib.Data.Int.Star
Mathlib.Geometry.Manifold.Complex
Mathlib.Geometry.Manifold.WhitneyEmbedding
Mathlib.LinearAlgebra.ExteriorPower.Basis
Mathlib.LinearAlgebra.Projectivization.Subspace
Mathlib.LinearAlgebra.QuadraticForm.Real
Mathlib.LinearAlgebra.QuadraticForm.Signature
Mathlib.NumberTheory.ModularForms.Derivative
Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
Mathlib.RingTheory.Etale.Weakly
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.RootsOfUnity.Complex
Mathlib.RingTheory.SimpleRing.Principal
Mathlib.Tactic.NormNum.Parity
Mathlib.Topology.Baire.LocallyCompactRegular
Mathlib.Topology.Connected.Separation
Mathlib.Topology.Homotopy.HomotopyGroup
Mathlib.Topology.MetricSpace.HausdorffDimension
Mathlib.Topology.Separation.Lemmas
Mathlib.Topology.Sheaves.EtaleSpace
Mathlib.Topology.UniformSpace.Ascoli
Mathlib.Topology.UniformSpace.Uniformizable
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.Biproducts
Mathlib.Algebra.Module.StablyFree.Basic
Mathlib.Algebra.Module.ZLattice.Summable
Mathlib.Analysis.Calculus.Deriv.Star
Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Mathlib.Analysis.Normed.Module.Connected
Mathlib.Analysis.Normed.Module.ContinuousInverse
Mathlib.Analysis.Normed.Module.Normalize
Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Mathlib.Analysis.SpecialFunctions.Pow.Integral
Mathlib.Geometry.Manifold.Instances.Icc
Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Mathlib.Geometry.Manifold.Sheaf.Basic
Mathlib.Geometry.Manifold.VectorField.Pullback
Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Mathlib.Order.Interval.Set.IsoIoo
Mathlib.Topology.Compactification.OnePoint.Sphere
Mathlib.Algebra.Order.Archimedean.Real.Hom
Std.Tactic.BVDecide.LRAT.Internal.Rup

Imported by

Hopf problem: prelude #

Supporting definitions and proofs for this stage of the six-sphere construction.