forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathCounterexamples.lean
More file actions
32 lines (31 loc) · 1.53 KB
/
Copy pathCounterexamples.lean
File metadata and controls
32 lines (31 loc) · 1.53 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
module -- shake: keep-all --deprecated_module: ignore
public import Counterexamples.AharoniKorman
public import Counterexamples.CanonicallyOrderedCommSemiringTwoMul
public import Counterexamples.CharPZeroNeCharZero
public import Counterexamples.CliffordAlgebraNotInjective
public import Counterexamples.Cyclotomic105
public import Counterexamples.DimensionPolynomial
public import Counterexamples.DirectSumIsInternal
public import Counterexamples.DiscreteTopologyNonDiscreteUniformity
public import Counterexamples.EulerSumOfPowers
public import Counterexamples.Girard
public import Counterexamples.GrothendieckPower
public import Counterexamples.HeawoodUnitDistance
public import Counterexamples.HomogeneousPrimeNotPrime
public import Counterexamples.InvertibleModuleNotIdeal
public import Counterexamples.IrrationalPowerOfIrrational
public import Counterexamples.MapFloor
public import Counterexamples.MonicNonRegular
public import Counterexamples.Motzkin
public import Counterexamples.NowhereDifferentiable
public import Counterexamples.OrderedCancelAddCommMonoidWithBounds
public import Counterexamples.PeanoCurve
public import Counterexamples.Phillips
public import Counterexamples.PolynomialIsDomain
public import Counterexamples.Pseudoelement
public import Counterexamples.QuadraticForm
public import Counterexamples.SeminormLatticeNotDistrib
public import Counterexamples.SeparableNotSecondCountable
public import Counterexamples.SorgenfreyLine
public import Counterexamples.TopologistsSineCurve
public import Counterexamples.ZeroDivisorsInAddMonoidAlgebras