Commit 6721c81
File tree
- .github
- workflows
- Archive
- Imo
- Wiedijk100Theorems
- Cache
- Counterexamples
- LongestPole
- Mathlib
- AlgebraicGeometry
- Cover
- EllipticCurve
- Affine
- DivisionPolynomial
- Jacobian
- Projective
- IdealSheaf
- Modules
- Morphisms
- ProjectiveSpectrum
- Sites
- AlgebraicTopology
- DoldKan
- FundamentalGroupoid
- ModelCategory
- Quasicategory
- RelativeCellComplex
- SimplexCategory
- Augmented
- GeneratorsRelations
- SimplicialObject
- SimplicialSet
- AnodyneExtensions
- Algebra
- AddConstMap
- AddTorsor
- Algebra
- Spectrum
- Subalgebra
- Azumaya
- BigOperators
- Finsupp
- GroupWithZero
- Group
- Finset
- List
- Multiset
- Ring
- BrauerGroup
- Category
- AlgCat
- CoalgCat
- FGModuleCat
- Grp
- ModuleCat
- Differentials
- Monoidal
- Presheaf
- Sheaf
- MonCat
- Ring
- Central
- CharP
- CharZero
- Colimit
- ContinuedFractions
- Computation
- DirectSum
- Divisibility
- EuclideanDomain
- Field
- Subfield
- FreeAbelianGroup
- GCDMonoid
- GroupWithZero
- Action
- Pointwise
- Pointwise/Set
- Submonoid
- Units
- Group
- Action
- Pointwise
- Set
- Commute
- Equiv
- Fin
- Hom
- Int
- Invertible
- Irreducible
- Nat
- Pi
- Pointwise
- Finset
- Set
- Semiconj
- Subgroup
- ZPowers
- Submonoid
- Subsemigroup
- TypeTags
- UniqueProds
- Units
- WithOne
- Homology
- DerivedCategory
- Ext
- Embedding
- HomotopyCategory
- LeftResolution
- ShortComplex
- Lie
- Derivation
- Weights
- Module
- Congruence
- Equiv
- LinearMap
- LocalizedModule
- Submodule
- Torsion
- ZLattice
- MonoidAlgebra
- MvPolynomial
- NoZeroSMulDivisors
- Notation
- Pi
- Order
- AbsoluteValue
- Antidiag
- Archimedean
- BigOperators
- Group
- Ring
- CauSeq
- Field
- Floor
- GroupWithZero
- Unbundled
- Group
- Int
- Pointwise
- Unbundled
- Hom
- Interval
- Finset
- Set
- Module
- Monoid
- Unbundled
- Nonneg
- Ring
- Ordering
- Unbundled
- Star
- Sub
- Unbundled
- WithTop
- Polynomial
- Degree
- Eval
- Module
- PresentedMonoid
- Prime
- QuadraticAlgebra
- Ring
- Action
- Pointwise
- Divisibility
- Hom
- Int
- Pointwise
- Subring
- Subsemiring
- SkewMonoidAlgebra
- SkewPolynomial
- Squarefree
- Star
- Tropical
- Vertex
- Analysis
- AbsoluteValue
- Analytic
- Asymptotics
- BoxIntegral
- Box
- CStarAlgebra
- ContinuousFunctionalCalculus
- Module
- Unitary
- Calculus
- AddTorsor
- BumpFunction
- Conformal
- ContDiff
- Deriv
- DifferentialForm
- FDeriv
- Gradient
- InverseFunctionTheorem
- IteratedDeriv
- LineDeriv
- LocalExtr
- TangentCone
- Complex
- Harmonic
- Polynomial
- UpperHalfPlane
- ValueDistribution
- Convex
- Cone
- SimplicialComplex
- SpecificFunctions
- Distribution
- Fourier
- FunctionalSpaces
- InnerProductSpace
- Harmonic
- Projection
- LocallyConvex
- Matrix
- Meromorphic
- NormedSpace
- Alternating
- Uncurry
- Multilinear
- PiTensorProduct
- Normed
- Affine
- Algebra
- Field
- Group
- Lp
- Module
- Ball
- RCLike
- Operator
- Order
- Ring
- Unbundled
- ODE
- Polynomial
- RCLike
- Real
- Pi
- SpecialFunctions
- Complex
- ContinuousFunctionalCalculus
- PosPart
- Rpow
- Gamma
- Gaussian
- Integrals
- Log
- Pow
- Trigonometric
- SpecificLimits
- CategoryTheory
- Abelian
- GrothendieckAxioms
- GrothendieckCategory
- ModuleEmbedding
- Injective
- Projective
- Action
- Adjunction
- Bicategory
- Adjunction
- FunctorBicategory
- Functor
- Kan
- Modification
- Monad
- NaturalTransformation
- Strict
- Category
- Cat
- Closed
- Comma
- Over
- StructuredArrow
- ConcreteCategory
- CopyDiscardCategory
- Dialectica
- Discrete
- EffectiveEpi
- Enriched
- Ordinary
- FiberedCategory
- Filtered
- Functor
- Derived
- KanExtension
- Galois
- Generator
- GradedObject
- Groupoid
- GuitartExact
- Idempotents
- Join
- LiftingProperties
- Limits
- ConcreteCategory
- Constructions
- Over
- Final
- FunctorCategory
- Shapes
- Indization
- Preserves
- Creates
- Shapes
- Shapes
- Opposites
- Preorder
- Pullback
- Categorical
- Types
- Linear
- Localization
- CalculusOfFractions
- DerivabilityStructure
- Monoidal
- LocallyCartesianClosed
- MarkovCategory
- Monad
- Monoidal
- Action
- Braided
- Cartesian
- DayConvolution
- Free
- Functor
- Internal
- Types
- Limits
- Opposite
- Rigid
- Types
- MorphismProperty
- ObjectProperty
- Preadditive
- Injective
- Projective
- Yoneda
- Presentable
- Products
- Shift
- Sites
- Coherent
- DenseSubsite
- Descent
- Hypercover
- NonabelianCohomology
- SheafCohomology
- SmallObject
- Iteration
- Subobject
- Subpresheaf
- Sums
- Triangulated
- Opposite
- TStructure
- Types
- WithTerminal
- Combinatorics
- Additive
- AP/Three
- Corner
- Derangements
- Digraph
- Enumerative
- Extremal
- Graph
- Hall
- Matroid
- Minor
- Rank
- Quiver
- SetFamily
- Compression
- SimpleGraph
- Connectivity
- Extremal
- Regularity
- Triangle
- Computability
- AkraBazzi
- Condensed
- Discrete
- Light
- Control
- Monad
- Data
- Array
- Bool
- Complex
- Countable
- DFinsupp
- ENNReal
- ENat
- EReal
- FP
- Finite
- Finset
- Lattice
- Finsupp
- MonomialOrder
- Fintype
- Fin
- Tuple
- Int
- Cast
- Order
- List
- Perm
- Matrix
- Multiset
- NNRat
- NNReal
- Nat
- Cast
- Order
- Choose
- Digits
- Factorial
- Factorization
- Fib
- GCD
- NthRoot
- Prime
- Num
- Option
- Ordmap
- PFunctor
- Multivariate
- Univariate
- PNat
- PSigma
- Prod
- QPF/Multivariate/Constructions
- Rat
- Cast
- Real
- Rel
- Seq
- SetLike
- Setoid
- Set
- Card
- Finite
- Lattice
- Pairwise
- Sigma
- Sign
- Stream
- String
- Sum
- Sym
- Sym2
- Tree
- Vector
- WSeq
- W
- ZMod
- Deprecated
- Dynamics
- BirkhoffSum
- Circle/RotationNumber
- Ergodic
- PeriodicPts
- TopologicalEntropy
- FieldTheory
- Differential
- Finite
- Galois
- IntermediateField
- Adjoin
- IsAlgClosed
- Minpoly
- Normal
- PurelyInseparable
- RatFunc
- SplittingField
- Geometry
- Convex/Cone
- Euclidean
- Angle
- Oriented
- Unoriented
- Inversion
- Sphere
- Group/Growth
- Manifold
- Algebra
- ContMDiff
- Instances
- IntegralCurve
- IsManifold
- MFDeriv
- Riemannian
- Sheaf
- VectorBundle
- VectorField
- RingedSpace
- GroupTheory
- Abelianization
- Congruence
- Coprod
- Coset
- Coxeter
- FiniteAbelian
- FreeGroup
- GroupAction
- DomAct
- SubMulAction
- MonoidLocalization
- OreLocalization
- Perm
- Cycle
- QuotientGroup
- SpecificGroups
- Alternating
- Subgroup
- Submonoid
- InformationTheory
- Lean
- Elab
- Expr
- Meta
- Tactic
- LinearAlgebra
- AffineSpace
- AffineSubspace
- Simplex
- Alternating/Uncurry
- Basis
- BilinearForm
- Charpoly
- CliffordAlgebra
- Complex
- Dimension
- Torsion
- DirectSum
- Dual
- Eigenspace
- FiniteDimensional
- Finsupp
- FreeModule
- Finite
- FreeProduct
- LinearIndependent
- Matrix
- Charpoly
- Determinant
- GeneralLinearGroup
- Irreducible
- Multilinear
- PerfectPairing
- Projectivization
- QuadraticForm
- QuadraticModuleCat
- TensorProduct
- Quotient
- RootSystem
- Finite
- GeckConstruction
- SModEq
- SesquilinearForm
- Span
- TensorAlgebra
- TensorProduct
- Graded
- Logic
- Embedding
- Equiv
- Fin
- Function
- Godel
- Nontrivial
- Small
- MeasureTheory
- Constructions
- BorelSpace
- Polish
- Covering
- Function
- AEEqFun
- ConditionalExpectation
- L1Space
- LpSeminorm
- LpSpace
- DomAct
- SpecialFunctions
- StronglyMeasurable
- Group
- Integral
- Bochner
- CurveIntegral
- IntervalIntegral
- Lebesgue
- RieszMarkovKakutani
- MeasurableSpace
- Measure
- Decomposition
- Haar
- Lebesgue
- Typeclasses
- OuterMeasure
- SpecificCodomains
- VectorMeasure
- Decomposition
- ModelTheory
- Algebra
- Field
- Ring
- Arithmetic/Presburger/Semilinear
- NumberTheory
- ClassNumber
- Cyclotomic
- DiophantineApproximation
- EulerProduct
- FLT
- Harmonic
- JacobiSum
- LSeries
- LegendreSymbol
- QuadraticChar
- LocalField
- ModularForms
- EisensteinSeries
- MulChar
- NumberField
- CanonicalEmbedding
- Cyclotomic
- Discriminant
- Ideal
- InfinitePlace
- Units
- Padics
- PadicVal
- RamificationInertia
- Real
- Transcendental/Liouville
- Zsqrtd
- Order
- BooleanAlgebra
- BoundedOrder
- Bounds
- Category
- CompactlyGenerated
- CompleteLattice
- ConditionallyCompleteLattice
- Defs
- Filter
- AtTopBot
- Bases
- Germ
- Fin
- GaloisConnection
- Heyting
- Hom
- Interval
- Finset
- Set
- Lattice
- Monotone
- Partition
- Preorder
- RelIso
- ScottContinuity
- SuccPred
- UpperLower
- Probability
- Decision/Risk
- Distributions
- Gaussian
- Independence
- Kernel
- Composition
- Disintegration
- IonescuTulcea
- Martingale
- Moments
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
11 | 11 | | |
12 | 12 | | |
13 | 13 | | |
14 | | - | |
15 | | - | |
16 | | - | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
17 | 23 | | |
18 | 24 | | |
19 | 25 | | |
20 | | - | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
21 | 30 | | |
22 | | - | |
23 | | - | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
24 | 34 | | |
25 | 35 | | |
26 | 36 | | |
| |||
Large diffs are not rendered by default.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
17 | 17 | | |
18 | 18 | | |
19 | 19 | | |
20 | | - | |
| 20 | + | |
21 | 21 | | |
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
25 | 25 | | |
26 | 26 | | |
27 | 27 | | |
28 | | - | |
| 28 | + | |
29 | 29 | | |
30 | 30 | | |
31 | 31 | | |
| |||
60 | 60 | | |
61 | 61 | | |
62 | 62 | | |
63 | | - | |
| 63 | + | |
64 | 64 | | |
65 | 65 | | |
66 | 66 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
10 | 10 | | |
11 | 11 | | |
12 | 12 | | |
13 | | - | |
| 13 | + | |
14 | 14 | | |
15 | 15 | | |
16 | | - | |
| 16 | + | |
17 | 17 | | |
18 | 18 | | |
19 | 19 | | |
| |||
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
25 | | - | |
| 25 | + | |
26 | 26 | | |
27 | 27 | | |
28 | 28 | | |
29 | 29 | | |
30 | 30 | | |
31 | 31 | | |
32 | 32 | | |
33 | | - | |
| 33 | + | |
34 | 34 | | |
35 | 35 | | |
36 | 36 | | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
25 | | - | |
| 25 | + | |
26 | 26 | | |
27 | 27 | | |
28 | 28 | | |
29 | 29 | | |
30 | | - | |
| 30 | + | |
31 | 31 | | |
32 | 32 | | |
33 | 33 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
11 | 11 | | |
12 | 12 | | |
13 | 13 | | |
14 | | - | |
| 14 | + | |
15 | 15 | | |
16 | 16 | | |
17 | 17 | | |
18 | 18 | | |
19 | 19 | | |
20 | 20 | | |
21 | | - | |
| 21 | + | |
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
10 | 10 | | |
11 | 11 | | |
12 | 12 | | |
13 | | - | |
| 13 | + | |
14 | 14 | | |
15 | 15 | | |
16 | 16 | | |
17 | 17 | | |
18 | 18 | | |
19 | 19 | | |
20 | | - | |
| 20 | + | |
21 | 21 | | |
22 | 22 | | |
23 | 23 | | |
| |||
0 commit comments