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
30 lines (30 loc) · 1.27 KB
/
Counterexamples.lean
File metadata and controls
30 lines (30 loc) · 1.27 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
import Counterexamples.AharoniKorman
import Counterexamples.CanonicallyOrderedCommSemiringTwoMul
import Counterexamples.CharPZeroNeCharZero
import Counterexamples.CliffordAlgebraNotInjective
import Counterexamples.Cyclotomic105
import Counterexamples.DimensionPolynomial
import Counterexamples.DirectSumIsInternal
import Counterexamples.DiscreteTopologyNonDiscreteUniformity
import Counterexamples.EulerSumOfPowers
import Counterexamples.GameMultiplication
import Counterexamples.Girard
import Counterexamples.HeawoodUnitDistance
import Counterexamples.HomogeneousPrimeNotPrime
import Counterexamples.InvertibleModuleNotIdeal
import Counterexamples.IrrationalPowerOfIrrational
import Counterexamples.MapFloor
import Counterexamples.MonicNonRegular
import Counterexamples.Motzkin
import Counterexamples.NowhereDifferentiable
import Counterexamples.OrderedCancelAddCommMonoidWithBounds
import Counterexamples.PeanoCurve
import Counterexamples.Phillips
import Counterexamples.PolynomialIsDomain
import Counterexamples.Pseudoelement
import Counterexamples.QuadraticForm
import Counterexamples.SeminormLatticeNotDistrib
import Counterexamples.SeparableNotSecondCountable
import Counterexamples.SorgenfreyLine
import Counterexamples.TopologistsSineCurve
import Counterexamples.ZeroDivisorsInAddMonoidAlgebras