-
0 dependencies
0 dependents
-
Affirming the consequent is a valid inference refuted · search-certificate · F:affirming-the-consequent C:fallacyC:converseC:countermodel +1 0 dependencies
0 dependents
-
The alternating binomial row sum vanishes proved · cas-certificate · F:alternating-binomial-row-sum-zero 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
No barber shaves exactly those who do not shave themselves proved · smt-clausal · F:barber-no-such-barber C:barber-paradoxC:russells-paradoxC:self-reference +2 0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
The binomial row sum is a power of two proved · cas-certificate · F:binomial-row-sum-two-power 0 dependencies
0 dependents
-
Boolean conjunction is commutative proved · imported-kernel-lean · F:bool-and-comm C:commutativityC:boolean-algebra 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
4 dependencies
0 dependents
-
16 dependencies
1 dependents
-
21 dependencies
1 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
Collatz conjecture conjectured · route not assigned · F:collatz-reaches-one C:collatz-conjectureC:collatz-sequenceC:parity 0 dependencies
0 dependents
-
32 dependencies
1 dependents
-
2 dependencies
1 dependents
-
12 dependencies
0 dependents
-
5 dependencies
0 dependents
-
14 dependencies
0 dependents
-
4 dependencies
1 dependents
-
7 dependencies
0 dependents
-
5 dependencies
4 dependents
-
Addition on the constructed complex numbers is commutative proved · kernel-lean · F:complex-add-comm C:commutativity 7 dependencies
1 dependents
-
1 dependencies
21 dependents
-
12 dependencies
1 dependents
-
6 dependencies
3 dependents
-
37 dependencies
0 dependents
-
5 dependencies
9 dependents
-
5 dependencies
0 dependents
-
15 dependencies
0 dependents
-
10 dependencies
0 dependents
-
16 dependencies
0 dependents
-
Complex conjugation is additive proved · kernel-lean · F:complex-conj-add C:complex-conjugate 9 dependencies
0 dependents
-
1 dependencies
0 dependents
-
9 dependencies
0 dependents
-
6 dependencies
0 dependents
-
7 dependencies
0 dependents
-
16 dependencies
1 dependents
-
Complex conjugation is multiplicative proved · kernel-lean · F:complex-conj-mul C:complex-conjugate 13 dependencies
2 dependents
-
7 dependencies
0 dependents
-
7 dependencies
1 dependents
-
5 dependencies
0 dependents
-
9 dependencies
0 dependents
-
7 dependencies
0 dependents
-
2 dependencies
0 dependents
-
6 dependencies
0 dependents
-
1 dependencies
1 dependents
-
20 dependencies
0 dependents
-
12 dependencies
1 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
37 dependents
-
Complex.Equiv is symmetric proved · kernel-lean · F:complex-equiv-symm 1 dependencies
19 dependents
-
Complex.Equiv is transitive proved · kernel-lean · F:complex-equiv-trans 1 dependencies
40 dependents
-
2 dependencies
0 dependents
-
12 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The complex finite geometric series as a quotient proved · kernel-lean · F:complex-geom-series-div C:geometric-series 9 dependencies
0 dependents
-
24 dependencies
0 dependents
-
hornerFromTop's diagonal equals polyEval: the sum-level bridge proved · kernel-lean · F:complex-hornerfromtop-diag-eq-polyeval 24 dependencies
0 dependents
-
0 dependencies
2 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
16 dependencies
0 dependents
-
The imaginary unit squares to negative one proved · kernel-lean · F:complex-i-sq C:imaginary-unit 12 dependencies
1 dependents
-
0 dependencies
0 dependents
-
4 dependencies
1 dependents
-
3 dependencies
2 dependents
-
8 dependencies
0 dependents
-
11 dependencies
4 dependents
-
12 dependencies
1 dependents
-
14 dependencies
5 dependents
-
12 dependencies
7 dependents
-
3 dependencies
17 dependents
-
15 dependencies
0 dependents
-
1 dependencies
1 dependents
-
13 dependencies
0 dependents
-
15 dependencies
3 dependents
-
11 dependencies
8 dependents
-
The complex finite geometric-sum identity proved · kernel-lean · F:complex-mul-sub-one-geom C:geometric-series 22 dependencies
2 dependents
-
5 dependencies
5 dependents
-
10 dependencies
5 dependents
-
1 dependencies
1 dependents
-
13 dependencies
1 dependents
-
7 dependencies
1 dependents
-
15 dependencies
1 dependents
-
2 dependencies
2 dependents
-
13 dependencies
3 dependents
-
2 dependencies
0 dependents
-
9 dependencies
2 dependents
-
15 dependencies
4 dependents
-
5 dependencies
3 dependents
-
10 dependencies
0 dependents
-
6 dependencies
2 dependents
-
8 dependencies
0 dependents
-
8 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
6 dependencies
1 dependents
-
11 dependencies
0 dependents
-
4 dependencies
1 dependents
-
0 dependencies
0 dependents
-
polyDegreeLt is closed under polyAdd at a shared bound proved · kernel-lean · F:complex-polydegreelt-polyadd 4 dependencies
0 dependents
-
28 dependencies
0 dependents
-
polyDegreeLt is closed under polyScale proved · kernel-lean · F:complex-polydegreelt-polyscale 4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
16 dependencies
0 dependents
-
44 dependencies
0 dependents
-
19 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
4 dependencies
2 dependents
-
6 dependencies
2 dependents
-
4 dependencies
1 dependents
-
0 dependencies
1 dependents
-
0 dependencies
1 dependents
-
15 dependencies
1 dependents
-
6 dependencies
0 dependents
-
12 dependencies
0 dependents
-
0 dependencies
0 dependents
-
15 dependencies
1 dependents
-
19 dependencies
0 dependents
-
7 dependencies
0 dependents
-
5 dependencies
0 dependents
-
11 dependencies
5 dependents
-
5 dependencies
4 dependents
-
3 dependencies
7 dependents
-
16 dependencies
1 dependents
-
4 dependencies
2 dependents
-
3 dependencies
1 dependents
-
4 dependencies
1 dependents
-
10 dependencies
2 dependents
-
5 dependencies
1 dependents
-
6 dependencies
2 dependents
-
0 dependencies
0 dependents
-
6 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The continuum hypothesis is independent of ZFC open · route not assigned · F:continuum-hypothesis-independent C:continuum-hypothesisC:independence-of-axiomsC:zfc-intuition +2 0 dependencies
0 dependents
-
A conditional is equivalent to its contrapositive proved · smt-term-level · F:contraposition C:contrapositiveC:logical-equivalenceC:converse 0 dependencies
1 dependents
-
8 dependencies
0 dependents
-
14 dependencies
0 dependents
-
20 dependencies
0 dependents
-
15 dependencies
0 dependents
-
The Cauchy-Schwarz inequality proved · kernel-lean · F:cpoint-cauchy-schwarz C:cauchy-schwarz-inequality 21 dependencies
1 dependents
-
22 dependencies
0 dependents
-
12 dependencies
0 dependents
-
19 dependencies
0 dependents
-
Ceva's theorem, sufficiency direction proved · kernel-lean · F:cpoint-ceva-concurrent-of-ratio-product C:cevas-theorem 16 dependencies
0 dependents
-
17 dependencies
0 dependents
-
16 dependencies
0 dependents
-
12 dependencies
1 dependents
-
8 dependencies
1 dependents
-
1 dependencies
1 dependents
-
16 dependencies
0 dependents
-
10 dependencies
3 dependents
-
16 dependencies
0 dependents
-
16 dependencies
0 dependents
-
16 dependencies
1 dependents
-
8 dependencies
0 dependents
-
7 dependencies
0 dependents
-
14 dependencies
0 dependents
-
15 dependencies
0 dependents
-
13 dependencies
6 dependents
-
3 dependencies
1 dependents
-
17 dependencies
0 dependents
-
2 dependencies
0 dependents
-
5 dependencies
1 dependents
-
7 dependencies
1 dependents
-
18 dependencies
0 dependents
-
8 dependencies
5 dependents
-
7 dependencies
7 dependents
-
The dot product on the constructed plane is commutative proved · kernel-lean · F:cpoint-dot-comm C:dot-product 2 dependencies
12 dependents
-
2 dependencies
21 dependents
-
14 dependencies
9 dependents
-
Polarization identity for the sum of two points proved · kernel-lean · F:cpoint-dot-self-add C:polarization-identity 7 dependencies
9 dependents
-
5 dependencies
1 dependents
-
A point's dot product with itself is non-negative proved · kernel-lean · F:cpoint-dot-self-nonneg C:non-negativity 6 dependencies
1 dependents
-
Polarization identity for the difference of two points proved · kernel-lean · F:cpoint-dot-self-sub C:polarization-identity 13 dependencies
10 dependents
-
2 dependencies
0 dependents
-
5 dependencies
2 dependents
-
14 dependencies
4 dependents
-
12 dependencies
5 dependents
-
9 dependencies
1 dependents
-
5 dependencies
2 dependents
-
The centroid vector identity anchoring the Euler line proved · kernel-lean · F:cpoint-euler-line C:eulers-line 15 dependencies
1 dependents
-
15 dependencies
0 dependents
-
15 dependencies
0 dependents
-
Lagrange's identity in two dimensions proved · kernel-lean · F:cpoint-lagrange-identity C:lagranges-identity 16 dependencies
0 dependents
-
17 dependencies
2 dependents
-
16 dependencies
1 dependents
-
10 dependencies
0 dependents
-
6 dependencies
0 dependents
-
15 dependencies
0 dependents
-
15 dependencies
0 dependents
-
18 dependencies
1 dependents
-
8 dependencies
0 dependents
-
14 dependencies
0 dependents
-
15 dependencies
1 dependents
-
15 dependencies
1 dependents
-
14 dependencies
1 dependents
-
7 dependencies
0 dependents
-
9 dependencies
0 dependents
-
The parallelogram law proved · kernel-lean · F:cpoint-parallelogram-law C:parallelogram-law 15 dependencies
0 dependents
-
13 dependencies
0 dependents
-
22 dependencies
1 dependents
-
20 dependencies
0 dependents
-
22 dependencies
0 dependents
-
6 dependencies
0 dependents
-
8 dependencies
1 dependents
-
The Pythagorean theorem restated in squared distance proved · kernel-lean · F:cpoint-pythagoras-distsq C:pythagorean-theorem 1 dependencies
0 dependents
-
The Pythagorean theorem proved · kernel-lean · F:cpoint-pythagoras C:pythagorean-theorem 14 dependencies
1 dependents
-
21 dependencies
1 dependents
-
12 dependencies
0 dependents
-
3 dependencies
0 dependents
-
6 dependencies
1 dependents
-
11 dependencies
0 dependents
-
10 dependencies
2 dependents
-
13 dependencies
1 dependents
-
6 dependencies
1 dependents
-
6 dependencies
2 dependents
-
5 dependencies
5 dependents
-
3 dependencies
16 dependents
-
Stewart's theorem specialised to the median proved · kernel-lean · F:cpoint-stewart-median C:stewarts-theorem 9 dependencies
1 dependents
-
Stewart's theorem proved · kernel-lean · F:cpoint-stewart C:stewarts-theorem 19 dependencies
1 dependents
-
22 dependencies
0 dependents
-
Thales' theorem (angle in a semicircle is a right angle) proved · kernel-lean · F:cpoint-thales C:thales-theorem 22 dependencies
0 dependents
-
7 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
10 dependencies
0 dependents
-
14 dependencies
18 dependents
-
2 dependencies
32 dependents
-
27 dependencies
1 dependents
-
25 dependencies
1 dependents
-
11 dependencies
1 dependents
-
13 dependencies
10 dependents
-
1 dependencies
58 dependents
-
28 dependencies
15 dependents
-
5 dependencies
14 dependents
-
16 dependencies
4 dependents
-
Addition on the constructed reals is associative proved · kernel-lean · F:creal-add-assoc C:associativity 14 dependencies
204 dependents
-
Addition on the constructed reals is commutative proved · kernel-lean · F:creal-add-comm C:commutativity 2 dependencies
241 dependents
-
Addition on the constructed reals respects CReal.Equiv proved · kernel-lean · F:creal-add-congr C:equivalence-relation 4 dependencies
261 dependents
-
4 dependencies
98 dependents
-
4 dependencies
5 dependents
-
2 dependencies
224 dependents
-
7 dependencies
35 dependents
-
9 dependencies
248 dependents
-
19 dependencies
1 dependents
-
19 dependencies
1 dependents
-
11 dependencies
0 dependents
-
9 dependencies
2 dependents
-
20 dependencies
2 dependents
-
7 dependencies
0 dependents
-
12 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
The constructed reals are Archimedean proved · kernel-lean · F:creal-archimedean C:archimedean-property 7 dependencies
3 dependents
-
13 dependencies
24 dependents
-
59 dependencies
4 dependents
-
19 dependencies
0 dependents
-
9 dependencies
1 dependents
-
8 dependencies
0 dependents
-
0 dependencies
6 dependents
-
13 dependencies
4 dependents
-
10 dependencies
4 dependents
-
40 dependencies
1 dependents
-
19 dependencies
1 dependents
-
14 dependencies
5 dependents
-
15 dependencies
4 dependents
-
15 dependencies
1 dependents
-
7 dependencies
2 dependents
-
9 dependencies
2 dependents
-
2 dependencies
1 dependents
-
20 dependencies
0 dependents
-
20 dependencies
0 dependents
-
11 dependencies
3 dependents
-
15 dependencies
1 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
14 dependencies
5 dependents
-
12 dependencies
1 dependents
-
8 dependencies
4 dependents
-
29 dependencies
1 dependents
-
12 dependencies
2 dependents
-
16 dependencies
5 dependents
-
7 dependencies
3 dependents
-
21 dependencies
4 dependents
-
3 dependencies
2 dependents
-
7 dependencies
5 dependents
-
3 dependencies
6 dependents
-
3 dependencies
5 dependents
-
0 dependencies
1 dependents
-
7 dependencies
1 dependents
-
10 dependencies
0 dependents
-
2 dependencies
1 dependents
-
A convergent sequence of constructed reals has a unique limit proved · kernel-lean · F:creal-converges-unique C:limit-of-a-sequence 7 dependencies
5 dependents
-
9 dependencies
7 dependents
-
22 dependencies
0 dependents
-
41 dependencies
0 dependents
-
12 dependencies
1 dependents
-
1 dependencies
2 dependents
-
18 dependencies
1 dependents
-
21 dependencies
1 dependents
-
17 dependencies
1 dependents
-
27 dependencies
1 dependents
-
27 dependencies
1 dependents
-
6 dependencies
0 dependents
-
40 dependencies
2 dependents
-
9 dependencies
0 dependents
-
cos(1)'s even-count partial sums are a lower bracket proved · kernel-lean · F:creal-cosone-alternating-lower 6 dependencies
1 dependents
-
cos(1)'s odd-count partial sums are an upper bracket proved · kernel-lean · F:creal-cosone-alternating-upper 6 dependencies
1 dependents
-
8 dependencies
0 dependents
-
32 dependencies
0 dependents
-
cos(1) is nonnegative: 0 <= cos(1) proved · kernel-lean · F:creal-cosone-nonneg 1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The cosine-at-1 partial sums converge to cosOne proved · kernel-lean · F:creal-cosoneconverges 27 dependencies
5 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
31 dependencies
4 dependents
-
16 dependencies
0 dependents
-
22 dependencies
1 dependents
-
0 dependencies
0 dependents
-
27 dependencies
1 dependents
-
9 dependencies
1 dependents
-
11 dependencies
2 dependents
-
14 dependencies
2 dependents
-
25 dependencies
1 dependents
-
2 dependencies
0 dependents
-
18 dependencies
1 dependents
-
27 dependencies
4 dependents
-
30 dependencies
0 dependents
-
39 dependencies
0 dependents
-
0 dependencies
0 dependents
-
8 dependencies
1 dependents
-
36 dependencies
4 dependents
-
1 dependencies
3 dependents
-
A uniform bound on the pointwise gap builds CReal.Equiv proved · kernel-lean · F:creal-equiv-of-bounded C:equivalence-relation 10 dependencies
8 dependents
-
2 dependencies
21 dependents
-
Pointwise-equal sequences build CReal.Equiv-equivalent reals proved · kernel-lean · F:creal-equiv-of-pointwise C:equivalence-relation 3 dependencies
15 dependents
-
CReal.Equiv is reflexive proved · kernel-lean · F:creal-equiv-refl C:equivalence-relation 3 dependencies
343 dependents
-
CReal.Equiv is symmetric proved · kernel-lean · F:creal-equiv-symm C:equivalence-relation 2 dependencies
294 dependents
-
CReal.Equiv is transitive proved · kernel-lean · F:creal-equiv-trans C:equivalence-relationC:transitivity 10 dependencies
316 dependents
-
15 dependencies
3 dependents
-
16 dependencies
7 dependents
-
16 dependencies
2 dependents
-
4 dependencies
0 dependents
-
23 dependencies
0 dependents
-
9 dependencies
1 dependents
-
9 dependencies
7 dependents
-
15 dependencies
3 dependents
-
7 dependencies
6 dependents
-
7 dependencies
1 dependents
-
41 dependencies
0 dependents
-
18 dependencies
1 dependents
-
27 dependencies
1 dependents
-
3 dependencies
0 dependents
-
3 dependencies
0 dependents
-
expTerm is antitone: 1/(n+1)! <= 1/n! proved · kernel-lean · F:creal-expterm-antitone 14 dependencies
4 dependents
-
1/n! is dominated by the geometric term 2/2^n proved · kernel-lean · F:creal-expterm-le-geom 16 dependencies
1 dependents
-
2 dependencies
0 dependents
-
expTerm(0) = 1 exactly, as a literal CReal equality proved · kernel-lean · F:creal-expterm-zero-eq-one 2 dependencies
0 dependents
-
13 dependencies
1 dependents
-
38 dependencies
1 dependents
-
24 dependencies
1 dependents
-
38 dependencies
1 dependents
-
34 dependencies
2 dependents
-
6 dependencies
2 dependents
-
12 dependencies
0 dependents
-
12 dependencies
1 dependents
-
12 dependencies
1 dependents
-
2 dependencies
1 dependents
-
21 dependencies
1 dependents
-
5 dependencies
1 dependents
-
20 dependencies
0 dependents
-
5 dependencies
1 dependents
-
6 dependencies
1 dependents
-
13 dependencies
2 dependents
-
20 dependencies
4 dependents
-
33 dependencies
6 dependents
-
3 dependencies
2 dependents
-
33 dependencies
1 dependents
-
7 dependencies
1 dependents
-
13 dependencies
1 dependents
-
12 dependencies
1 dependents
-
31 dependencies
3 dependents
-
46 dependencies
1 dependents
-
8 dependencies
0 dependents
-
44 dependencies
1 dependents
-
25 dependencies
3 dependents
-
8 dependencies
6 dependents
-
17 dependencies
3 dependents
-
4 dependencies
0 dependents
-
17 dependencies
4 dependents
-
24 dependencies
0 dependents
-
41 dependencies
3 dependents
-
20 dependencies
5 dependents
-
7 dependencies
0 dependents
-
17 dependencies
1 dependents
-
21 dependencies
2 dependents
-
27 dependencies
3 dependents
-
2 dependencies
6 dependents
-
38 dependencies
1 dependents
-
48 dependencies
0 dependents
-
0 dependencies
13 dependents
-
22 dependencies
3 dependents
-
23 dependencies
1 dependents
-
5 dependencies
2 dependents
-
13 dependencies
0 dependents
-
5 dependencies
4 dependents
-
2 dependencies
8 dependents
-
29 dependencies
1 dependents
-
Order passes to the integral proved · kernel-lean · F:creal-integral-le 21 dependencies
2 dependents
-
A constant factor pulls out of the integral proved · kernel-lean · F:creal-integral-scale 27 dependencies
0 dependents
-
39 dependencies
1 dependents
-
19 dependencies
1 dependents
-
4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
73 dependencies
1 dependents
-
39 dependencies
2 dependents
-
59 dependencies
1 dependents
-
8 dependencies
3 dependents
-
2 dependencies
0 dependents
-
18 dependencies
4 dependents
-
22 dependencies
0 dependents
-
14 dependencies
2 dependents
-
38 dependencies
0 dependents
-
38 dependencies
2 dependents
-
11 dependencies
1 dependents
-
2 dependencies
1 dependents
-
37 dependencies
1 dependents
-
16 dependencies
0 dependents
-
18 dependencies
0 dependents
-
33 dependencies
1 dependents
-
9 dependencies
1 dependents
-
27 dependencies
1 dependents
-
1 dependencies
42 dependents
-
13 dependencies
2 dependents
-
12 dependencies
6 dependents
-
3 dependencies
158 dependents
-
5 dependencies
11 dependents
-
5 dependencies
9 dependents
-
1 dependencies
9 dependents
-
0 dependencies
42 dependents
-
14 dependencies
3 dependents
-
14 dependencies
4 dependents
-
3 dependencies
31 dependents
-
11 dependencies
5 dependents
-
3 dependencies
1 dependents
-
2 dependencies
118 dependents
-
The order on the constructed reals is transitive proved · kernel-lean · F:creal-le-trans C:order-relationC:transitivity 7 dependencies
136 dependents
-
17 dependencies
123 dependents
-
13 dependencies
0 dependents
-
8 dependencies
0 dependents
-
26 dependencies
1 dependents
-
5 dependencies
14 dependents
-
20 dependencies
8 dependents
-
17 dependencies
7 dependents
-
3 dependencies
3 dependents
-
1 dependencies
5 dependents
-
2 dependencies
2 dependents
-
8 dependencies
0 dependents
-
14 dependencies
0 dependents
-
4 dependencies
5 dependents
-
1 dependencies
13 dependents
-
4 dependencies
1 dependents
-
24 dependencies
1 dependents
-
2 dependencies
1 dependents
-
2 dependencies
1 dependents
-
0 dependencies
0 dependents
-
6 dependencies
1 dependents
-
3 dependencies
1 dependents
-
0 dependencies
0 dependents
-
13 dependencies
12 dependents
-
24 dependencies
3 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
2 dependencies
0 dependents
-
22 dependencies
1 dependents
-
6 dependencies
3 dependents
-
10 dependencies
0 dependents
-
4 dependencies
0 dependents
-
5 dependencies
8 dependents
-
5 dependencies
10 dependents
-
4 dependencies
1 dependents
-
2 dependencies
3 dependents
-
48 dependencies
3 dependents
-
Multiplication on the constructed reals is associative proved · kernel-lean · F:creal-mul-assoc C:associativity 16 dependencies
97 dependents
-
Multiplication on the constructed reals is commutative proved · kernel-lean · F:creal-mul-comm C:commutativity 4 dependencies
169 dependents
-
Multiplication on the constructed reals respects CReal.Equiv proved · kernel-lean · F:creal-mul-congr C:equivalence-relation 15 dependencies
185 dependents
-
A constructed real bounded away from zero has a multiplicative inverse proved · kernel-lean · F:creal-mul-inv-cancel C:multiplicative-inverse 30 dependencies
31 dependents
-
14 dependencies
57 dependents
-
17 dependencies
35 dependents
-
8 dependencies
119 dependents
-
14 dependencies
2 dependents
-
5 dependencies
1 dependents
-
16 dependencies
2 dependents
-
51 dependencies
2 dependents
-
15 dependencies
1 dependents
-
14 dependencies
2 dependents
-
5 dependencies
16 dependents
-
2 dependencies
99 dependents
-
3 dependencies
2 dependents
-
21 dependencies
0 dependents
-
6 dependencies
1 dependents
-
1 dependencies
1 dependents
-
1 dependencies
1 dependents
-
14 dependencies
2 dependents
-
Negation on the constructed reals respects CReal.Equiv proved · kernel-lean · F:creal-neg-congr C:equivalence-relation 3 dependencies
129 dependents
-
34 dependencies
0 dependents
-
1 dependencies
39 dependents
-
1 dependencies
44 dependents
-
5 dependencies
4 dependents
-
8 dependencies
13 dependents
-
7 dependencies
3 dependents
-
7 dependencies
0 dependents
-
4 dependencies
0 dependents
-
5 dependencies
0 dependents
-
4 dependencies
0 dependents
-
3 dependencies
1 dependents
-
8 dependencies
1 dependents
-
3 dependencies
5 dependents
-
3 dependencies
9 dependents
-
3 dependencies
3 dependents
-
1 dependencies
51 dependents
-
5 dependencies
94 dependents
-
1 dependencies
47 dependents
-
1 dependencies
7 dependents
-
4 dependencies
9 dependents
-
4 dependencies
2 dependents
-
1 dependencies
2 dependents
-
10 dependencies
0 dependents
-
3 dependencies
0 dependents
-
4 dependencies
0 dependents
-
0 dependencies
3 dependents
-
0 dependencies
0 dependents
-
4 dependencies
0 dependents
-
polyDegreeLt is closed under polyScale proved · kernel-lean · F:creal-polydegreelt-polyscale 4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
7 dependencies
0 dependents
-
6 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
9 dependencies
7 dependents
-
7 dependencies
0 dependents
-
6 dependencies
4 dependents
-
2 dependencies
4 dependents
-
28 dependencies
4 dependents
-
36 dependencies
1 dependents
-
39 dependencies
1 dependents
-
8 dependencies
6 dependents
-
6 dependencies
3 dependents
-
5 dependencies
1 dependents
-
8 dependencies
0 dependents
-
3 dependencies
26 dependents
-
2 dependencies
0 dependents
-
13 dependencies
1 dependents
-
11 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
13 dependencies
1 dependents
-
3 dependencies
2 dependents
-
0 dependencies
0 dependents
-
16 dependencies
0 dependents
-
7 dependencies
2 dependents
-
11 dependencies
3 dependents
-
11 dependencies
3 dependents
-
3 dependencies
2 dependents
-
11 dependencies
1 dependents
-
14 dependencies
8 dependents
-
5 dependencies
1 dependents
-
1 dependencies
27 dependents
-
29 dependencies
1 dependents
-
1 dependencies
5 dependents
-
5 dependencies
3 dependents
-
0 dependencies
50 dependents
-
1 dependencies
0 dependents
-
7 dependencies
1 dependents
-
18 dependencies
6 dependents
-
19 dependencies
1 dependents
-
4 dependencies
0 dependents
-
14 dependencies
1 dependents
-
11 dependencies
0 dependents
-
18 dependencies
1 dependents
-
27 dependencies
10 dependents
-
5 dependencies
0 dependents
-
11 dependencies
3 dependents
-
31 dependencies
1 dependents
-
16 dependencies
0 dependents
-
19 dependencies
1 dependents
-
27 dependencies
1 dependents
-
12 dependencies
1 dependents
-
12 dependencies
1 dependents
-
13 dependencies
1 dependents
-
13 dependencies
1 dependents
-
23 dependencies
7 dependents
-
12 dependencies
1 dependents
-
9 dependencies
6 dependents
-
15 dependencies
0 dependents
-
9 dependencies
7 dependents
-
15 dependencies
2 dependents
-
3 dependencies
8 dependents
-
22 dependencies
0 dependents
-
1 dependencies
1 dependents
-
21 dependencies
1 dependents
-
43 dependencies
2 dependents
-
9 dependencies
0 dependents
-
sin(1)'s even-count partial sums are a lower bracket proved · kernel-lean · F:creal-sinone-alternating-lower 6 dependencies
1 dependents
-
sin(1)'s odd-count partial sums are an upper bracket proved · kernel-lean · F:creal-sinone-alternating-upper 6 dependencies
1 dependents
-
8 dependencies
0 dependents
-
sin(1) is nonnegative: 0 <= sin(1) proved · kernel-lean · F:creal-sinone-nonneg 1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
27 dependencies
2 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
32 dependencies
1 dependents
-
1 dependencies
6 dependents
-
61 dependencies
1 dependents
-
5 dependencies
8 dependents
-
42 dependencies
5 dependents
-
39 dependencies
2 dependents
-
11 dependencies
1 dependents
-
4 dependencies
1 dependents
-
28 dependencies
1 dependents
-
53 dependencies
3 dependents
-
17 dependencies
0 dependents
-
40 dependencies
0 dependents
-
22 dependencies
7 dependents
-
15 dependencies
0 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
48 dependencies
2 dependents
-
51 dependencies
3 dependents
-
26 dependencies
4 dependents
-
7 dependencies
5 dependents
-
12 dependencies
6 dependents
-
7 dependencies
1 dependents
-
Absolute convergence implies convergence, Cauchy form proved · kernel-lean · F:creal-sumrange-cauchy-of-abs-cauchy 2 dependencies
1 dependents
-
5 dependencies
3 dependents
-
The comparison test for series of nonnegative terms proved · kernel-lean · F:creal-sumrange-comparisontest 12 dependencies
0 dependents
-
3 dependencies
9 dependents
-
13 dependencies
6 dependents
-
Absolute convergence implies convergence, Converges form proved · kernel-lean · F:creal-sumrange-converges-of-abs-converges 3 dependencies
0 dependents
-
2 dependencies
2 dependents
-
4 dependencies
0 dependents
-
4 dependencies
11 dependents
-
6 dependencies
3 dependents
-
24 dependencies
3 dependents
-
4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
6 dependencies
7 dependents
-
0 dependencies
0 dependents
-
3 dependencies
1 dependents
-
14 dependencies
1 dependents
-
6 dependencies
1 dependents
-
2 dependencies
0 dependents
-
7 dependencies
2 dependents
-
4 dependencies
3 dependents
-
4 dependencies
0 dependents
-
8 dependencies
2 dependents
-
0 dependencies
0 dependents
-
3 dependencies
0 dependents
-
18 dependencies
1 dependents
-
45 dependencies
1 dependents
-
0 dependencies
3 dependents
-
15 dependencies
0 dependents
-
2 dependencies
0 dependents
-
1 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
2 <= e, by an EVENTUAL argument proved · kernel-lean · F:creal-two-le-e 8 dependencies
0 dependents
-
2 <= pi, the cheapest honest lower bound proved · kernel-lean · F:creal-two-le-pi 13 dependencies
0 dependents
-
14 dependencies
4 dependents
-
Uniform convergence is closed under termwise addition proved · kernel-lean · F:creal-uniform-converges-add 18 dependencies
0 dependents
-
x*(1/2)^n converges uniformly to the zero function on [0,1] proved · kernel-lean · F:creal-uniform-converges-geom-half 20 dependencies
0 dependents
-
16 dependencies
0 dependents
-
19 dependencies
2 dependents
-
15 dependencies
1 dependents
-
0 dependencies
7 dependents
-
0 dependencies
0 dependents
-
4 dependencies
1 dependents
-
23 dependencies
5 dependents
-
12 dependencies
9 dependents
-
0 dependencies
8 dependents
-
40 dependencies
5 dependents
-
15 dependencies
1 dependents
-
5 dependencies
0 dependents
-
2 dependencies
1 dependents
-
2 dependencies
2 dependents
-
2 dependencies
4 dependents
-
0 dependencies
19 dependents
-
40 dependencies
5 dependents
-
3 dependencies
2 dependents
-
4 dependencies
21 dependents
-
0 dependencies
0 dependents
-
De Morgan's laws for conjunction and disjunction proved · smt-term-level · F:de-morgan-laws C:de-morgans-lawsC:logical-equivalenceC:negation 0 dependencies
0 dependents
-
3 dependencies
0 dependents
-
12 dependencies
0 dependents
-
Double negation elimination proved · smt-term-level · F:double-negation-elimination C:negationC:proof-by-contradictionC:non-constructive-proof +1 1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
Mathlib's Extreme Value Theorem, imported (labeled scaffolding, not ours) proved · imported-kernel-lean · F:evt-mathlib-import-compact-exists-is-max-on 0 dependencies
0 dependents
-
A contradiction entails everything proved · smt-term-level · F:ex-falso-quodlibet C:contradiction-logicalC:proof-by-contradictionC:consistency 0 dependencies
0 dependents
-
Excluded middle is not derivable in intuitionistic propositional logic proved · kernel-lean · F:excluded-middle-not-intuitionistic C:intuitionismC:excluded-middleC:non-constructive-proof +2 2 dependencies
0 dependents
-
Law of excluded middle proved · smt-term-level · F:excluded-middle C:excluded-middleC:intuitionismC:truth-value 0 dependencies
2 dependents
-
Exportation: the propositional form of the deduction theorem proved · smt-term-level · F:exportation C:deductionC:implicationC:assumption +1 0 dependencies
0 dependents
-
2 dependencies
1 dependents
-
Fermat's Last Theorem open · route not assigned · F:fermat-last-theorem C:fermats-last-theorem 0 dependencies
0 dependents
-
7 dependencies
2 dependents
-
4 dependencies
0 dependents
-
6 dependencies
1 dependents
-
Validity in first-order logic is undecidable open · route not assigned · F:fol-validity-undecidable C:halting-problem-logicC:undecidable-statementC:computable-function +3 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Narrowing binary16 to bfloat16 and back is the identity refuted · search-certificate · F:fp16-bf16-roundtrip-not-identity 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The Franel numbers satisfy a second-order recurrence proved · cas-certificate · F:franel-numbers-recurrence 0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
the medians of a non-degenerate triangle meet at (A+B+C)/3 proved · cas-certificate · F:geometry-centroid-divides-medians 0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
the medians of a triangle are concurrent proved · cas-certificate · F:geometry-medians-concurrent 0 dependencies
1 dependents
-
the altitudes of a triangle are concurrent proved · cas-certificate · F:geometry-orthocentre-altitudes-concurrent 0 dependencies
1 dependents
-
1 dependencies
2 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
the diagonals of a non-flat parallelogram bisect each other proved · cas-certificate · F:geometry-parallelogram-diagonals-bisect 0 dependencies
1 dependents
-
2 dependencies
0 dependents
-
the diagonals of a non-flat rhombus are perpendicular proved · cas-certificate · F:geometry-rhombus-diagonals-perpendicular 0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
19 dependencies
1 dependents
-
1 dependencies
0 dependents
-
Thales' theorem: an angle inscribed in a semicircle is right proved · cas-certificate · F:geometry-thales-right-angle-in-semicircle 0 dependencies
1 dependents
-
Varignon's theorem: the midpoint quadrilateral is a parallelogram proved · cas-certificate · F:geometry-varignon-midpoint-parallelogram 0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
Binary irreducible monomial composition criterion and iteration proved · cas-certificate · F:gf2-general-monomial-composition-criterion 0 dependencies
0 dependents
-
Degree-seven joint Witt shifted-trace closed form proved · cas-certificate · F:gf2-witt-shifted-degree-seven-closed-form 0 dependencies
0 dependents
-
Godel's first incompleteness theorem open · route not assigned · F:godel-first-incompleteness C:godel-incompletenessC:incompleteness-theoremC:completeness-logical +4 0 dependencies
0 dependents
-
Strong Goldbach conjecture conjectured · route not assigned · F:goldbach-strong C:goldbach-conjectureC:prime-number 0 dependencies
0 dependents
-
The 3-element Gödel/Łukasiewicz Heyting chain refutes excluded middle proved · kernel-lean · F:heyting-3-chain-refutes-excluded-middle C:intuitionismC:excluded-middleC:non-constructive-proof 0 dependencies
1 dependents
-
Addition on the integers is associative proved · kernel-lean · F:int-add-assoc C:associativityC:integers 9 dependencies
56 dependents
-
Addition on the integers is commutative proved · kernel-lean · F:int-add-comm C:commutativityC:integers 2 dependencies
83 dependents
-
The order on the integers is compatible with addition proved · kernel-lean · F:int-add-le-add C:ordered-ringC:integers 4 dependencies
16 dependents
-
A strict integer inequality survives addition of a non-strict one proved · kernel-lean · F:int-add-lt-add-of-le-of-lt C:ordered-ringC:integers 6 dependencies
5 dependents
-
2 dependencies
2 dependents
-
2 dependencies
0 dependents
-
4 dependencies
25 dependents
-
Every integer has an additive inverse proved · kernel-lean · F:int-add-neg C:additive-inverseC:integers 1 dependencies
46 dependents
-
0 dependencies
76 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
10 dependencies
0 dependents
-
5 dependencies
1 dependents
-
2 dependencies
2 dependents
-
7 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
2 dependents
-
5 dependencies
1 dependents
-
3 dependencies
0 dependents
-
0 dependencies
1 dependents
-
3 dependencies
1 dependents
-
2 dependencies
3 dependents
-
0 dependencies
3 dependents
-
1 dependencies
1 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
1 dependents
-
0 dependencies
2 dependents
-
2 dependencies
1 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
2 dependencies
1 dependents
-
7 dependencies
5 dependents
-
2 dependencies
1 dependents
-
13 dependencies
0 dependents
-
9 dependencies
0 dependents
-
1 dependencies
7 dependents
-
8 dependencies
1 dependents
-
4 dependencies
2 dependents
-
1 dependencies
4 dependents
-
0 dependencies
7 dependents
-
2 dependencies
14 dependents
-
1 dependencies
7 dependents
-
1 dependencies
11 dependents
-
11 dependencies
36 dependents
-
18 dependencies
16 dependents
-
7 dependencies
4 dependents
-
10 dependencies
18 dependents
-
0 dependencies
2 dependents
-
6 dependencies
19 dependents
-
Equality of integers is decidable proved · kernel-lean · F:int-equality-is-decidable C:decidabilityC:integers 3 dependencies
8 dependents
-
1 dependencies
0 dependents
-
4 dependencies
4 dependents
-
14 dependencies
1 dependents
-
3 dependencies
1 dependents
-
Euclidean decomposition over the integers is derived, not assumed proved · kernel-lean · F:int-euclidean-decomposition C:euclidean-division 6 dependencies
1 dependents
-
11 dependencies
1 dependents
-
33 dependencies
0 dependents
-
29 dependencies
1 dependents
-
30 dependencies
0 dependents
-
22 dependencies
1 dependents
-
21 dependencies
1 dependents
-
9 dependencies
1 dependents
-
5 dependencies
1 dependents
-
4 dependencies
1 dependents
-
1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
36 dependencies
2 dependents
-
5 dependencies
0 dependents
-
29 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
2 dependencies
1 dependents
-
14 dependencies
3 dependents
-
23 dependencies
0 dependents
-
3 dependencies
0 dependents
-
8 dependencies
6 dependents
-
17 dependencies
2 dependents
-
1 dependencies
1 dependents
-
7 dependencies
1 dependents
-
gcd is commutative on the integers proved · kernel-lean · F:int-gcd-comm C:greatest-common-divisor 10 dependencies
1 dependents
-
2 dependencies
11 dependents
-
2 dependencies
11 dependents
-
9 dependencies
4 dependents
-
2 dependencies
0 dependents
-
11 dependencies
2 dependents
-
8 dependencies
0 dependents
-
3 dependencies
0 dependents
-
2 dependencies
0 dependents
-
1 dependencies
1 dependents
-
4 dependencies
3 dependents
-
5 dependencies
5 dependents
-
1 dependencies
8 dependents
-
5 dependencies
4 dependents
-
The integer order is reflexive proved · kernel-lean · F:int-le-refl 0 dependencies
28 dependents
-
The integer order is total proved · kernel-lean · F:int-le-total 1 dependencies
11 dependents
-
The integer order is transitive proved · kernel-lean · F:int-le-trans 1 dependencies
5 dependents
-
Multiplication distributes over addition on the integers proved · kernel-lean · F:int-left-distrib C:distributivityC:integers 8 dependencies
37 dependents
-
1 dependencies
0 dependents
-
6 dependencies
6 dependents
-
1 dependencies
34 dependents
-
2 dependencies
3 dependents
-
1 dependencies
8 dependents
-
2 dependencies
5 dependents
-
7 dependencies
4 dependents
-
2 dependencies
2 dependents
-
3 dependencies
1 dependents
-
2 dependencies
7 dependents
-
14 dependencies
16 dependents
-
13 dependencies
9 dependents
-
6 dependencies
5 dependents
-
11 dependencies
23 dependents
-
5 dependencies
3 dependents
-
10 dependencies
4 dependents
-
6 dependencies
12 dependents
-
2 dependencies
4 dependents
-
3 dependencies
13 dependents
-
1 dependencies
1 dependents
-
6 dependencies
2 dependents
-
1 dependencies
0 dependents
-
4 dependencies
0 dependents
-
2 dependencies
2 dependents
-
4 dependencies
3 dependents
-
2 dependencies
1 dependents
-
Congruence mod n is reflexive on the integers proved · kernel-lean · F:int-modeq-refl C:modular-arithmeticC:congruence 0 dependencies
14 dependents
-
6 dependencies
0 dependents
-
4 dependencies
0 dependents
-
Congruence mod n is symmetric on the integers proved · kernel-lean · F:int-modeq-symm C:modular-arithmeticC:congruence 1 dependencies
31 dependents
-
Congruence mod n is transitive on the integers proved · kernel-lean · F:int-modeq-trans C:modular-arithmeticC:congruence 1 dependencies
25 dependents
-
3 dependencies
1 dependents
-
Multiplication on the integers is associative proved · kernel-lean · F:int-mul-assoc C:associativityC:integers 5 dependencies
68 dependents
-
Multiplication on the integers is commutative proved · kernel-lean · F:int-mul-comm C:commutativityC:integers 1 dependencies
85 dependents
-
3 dependencies
4 dependents
-
6 dependencies
7 dependents
-
6 dependencies
6 dependents
-
1 dependencies
2 dependents
-
1 dependencies
3 dependents
-
0 dependencies
4 dependents
-
3 dependencies
15 dependents
-
1 dependencies
12 dependents
-
0 dependencies
2 dependents
-
1 dependencies
54 dependents
-
3 dependencies
4 dependents
-
2 dependencies
8 dependents
-
0 dependencies
33 dependents
-
1 dependencies
20 dependents
-
1 dependencies
16 dependents
-
0 dependencies
4 dependents
-
1 dependencies
3 dependents
-
2 dependencies
0 dependents
-
2 dependencies
0 dependents
-
4 dependencies
2 dependents
-
2 dependencies
3 dependents
-
Multiplying by negative one is negation proved · kernel-lean · F:int-neg-one-mul 3 dependencies
24 dependents
-
2 dependencies
2 dependents
-
4 dependencies
1 dependents
-
9 dependencies
1 dependents
-
No integer lies strictly between zero and one proved · kernel-lean · F:int-no-integer-strictly-between-zero-and-one C:discretenessC:integers 4 dependencies
2 dependents
-
1 dependencies
0 dependents
-
0 dependencies
3 dependents
-
1 dependencies
5 dependents
-
7 dependencies
3 dependents
-
4 dependencies
1 dependents
-
0 dependencies
17 dependents
-
0 dependencies
1 dependents
-
2 dependencies
21 dependents
-
3 dependencies
4 dependents
-
1 dependencies
0 dependents
-
8 dependencies
3 dependents
-
8 dependencies
2 dependents
-
12 dependencies
3 dependents
-
0 dependencies
9 dependents
-
0 dependencies
2 dependents
-
25 dependencies
1 dependents
-
2 dependencies
0 dependents
-
2 dependencies
4 dependents
-
0 dependencies
3 dependents
-
0 dependencies
1 dependents
-
3 dependencies
4 dependents
-
19 dependencies
4 dependents
-
2 dependencies
2 dependents
-
3 dependencies
3 dependents
-
2 dependencies
1 dependents
-
0 dependencies
0 dependents
-
9 dependencies
1 dependents
-
18 dependencies
3 dependents
-
0 dependencies
0 dependents
-
1 dependencies
2 dependents
-
16 dependencies
1 dependents
-
3 dependencies
1 dependents
-
2 dependencies
1 dependents
-
2 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The law of quadratic reciprocity proved · kernel-lean · F:int-quadratic-reciprocity 6 dependencies
0 dependents
-
10 dependencies
0 dependents
-
16 dependencies
2 dependents
-
Every integer square is nonnegative proved · kernel-lean · F:int-sq-nonneg C:integers 2 dependencies
2 dependents
-
2 dependencies
6 dependents
-
6 dependencies
3 dependents
-
4 dependencies
2 dependents
-
2 dependencies
9 dependents
-
6 dependencies
11 dependents
-
The normalized integer difference is invariant under a common shift proved · kernel-lean · F:int-sub-nat-nat-shift C:integersC:natural-numbers 2 dependencies
3 dependents
-
1 dependencies
2 dependents
-
3 dependencies
4 dependents
-
2 dependencies
3 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
3 dependencies
1 dependents
-
0 dependencies
1 dependents
-
Negation pulls out of a signed finite sum proved · kernel-lean · F:int-sumrange-neg 2 dependencies
1 dependents
-
0 dependencies
0 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
19 dependencies
1 dependents
-
2 dependencies
0 dependents
-
22 dependencies
2 dependents
-
30 dependencies
1 dependents
-
0 dependencies
16 dependents
-
0 dependencies
2 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
The empty list is a left identity for append proved · imported-kernel-lean · F:list-nil-append C:identity-element 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Conjunction: left projection proved · kernel-lean · F:logic-and-left 0 dependencies
22 dependents
-
Conjunction: right projection proved · kernel-lean · F:logic-and-right 0 dependencies
21 dependents
-
Boolean false is not true proved · kernel-lean · F:logic-bool-false-ne-true 0 dependencies
8 dependents
-
Boolean true is not false proved · kernel-lean · F:logic-bool-true-ne-false 2 dependencies
4 dependents
-
1 dependencies
0 dependents
-
Excluded middle for decidable propositions proved · kernel-lean · F:logic-decidable-em 0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
De Morgan: not-p and not-q implies not-(p or q) proved · kernel-lean · F:logic-demorgan-not-or-converse 3 dependencies
0 dependents
-
De Morgan: not-(p or q) implies not-p and not-q proved · kernel-lean · F:logic-demorgan-not-or 0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
Excluded middle from Peirce's law proved · kernel-lean · F:logic-em-of-peirce 0 dependencies
0 dependents
-
Biconditional: forward direction proved · kernel-lean · F:logic-iff-mp 0 dependencies
17 dependents
-
Biconditional: backward direction proved · kernel-lean · F:logic-iff-mpr 0 dependencies
19 dependents
-
Modus tollens (kernel route) proved · kernel-lean · F:logic-modus-tollens 0 dependencies
0 dependents
-
Law of non-contradiction (kernel route) proved · kernel-lean · F:logic-noncontradiction 2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Excluded middle is irrefutable proved · kernel-lean · F:logic-not-not-em 0 dependencies
1 dependents
-
Double-negation introduction proved · kernel-lean · F:logic-not-not-intro 0 dependencies
2 dependents
-
1 dependencies
0 dependents
-
Disjunction elimination (case analysis) proved · kernel-lean · F:logic-or-elim 0 dependencies
19 dependents
-
Disjunctive syllogism (left) proved · kernel-lean · F:logic-or-resolve-left 0 dependencies
1 dependents
-
Peirce's law from excluded middle proved · kernel-lean · F:logic-peirce-of-em 1 dependencies
0 dependents
-
15 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_assoc proved · kernel-lean · F:ml430-int-add-assoc-749cb0ff 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.add_comm proved · kernel-lean · F:ml430-int-add-comm-c5722728 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.add_ediv_of_dvd_left open · route not assigned · F:ml430-int-add-ediv-of-dvd-left-52ee6c5c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_ediv_of_dvd_right open · route not assigned · F:ml430-int-add-ediv-of-dvd-right-3ead15d8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod open · route not assigned · F:ml430-int-add-emod-b5735756 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod_emod open · route not assigned · F:ml430-int-add-emod-emod-87d0ffc8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod_eq_add_emod_left open · route not assigned · F:ml430-int-add-emod-eq-add-emod-left-71885891 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod_eq_add_emod_right open · route not assigned · F:ml430-int-add-emod-eq-add-emod-right-c2cf373e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod_left open · route not assigned · F:ml430-int-add-emod-left-dd3f807c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_emod_right open · route not assigned · F:ml430-int-add-emod-right-4345648e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_add proved · kernel-lean · F:ml430-int-add-le-add-a76ad5ce 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_add_iff_left proved · kernel-lean · F:ml430-int-add-le-add-iff-left-83bf44fa 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_add_iff_right proved · kernel-lean · F:ml430-int-add-le-add-iff-right-995cbaa5 3 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.add_le_add_left proved · kernel-lean · F:ml430-int-add-le-add-left-4a766697 2 dependencies
5 dependents
-
Mathlib v4.30 source proposition Int.add_le_add_right proved · kernel-lean · F:ml430-int-add-le-add-right-0c9ed495 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.add_le_add_three proved · kernel-lean · F:ml430-int-add-le-add-three-ade2c97e 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_iff_le_sub proved · kernel-lean · F:ml430-int-add-le-iff-le-sub-66d51eea 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_of_le_neg_add proved · kernel-lean · F:ml430-int-add-le-of-le-neg-add-6481d6ea 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_of_le_sub_left proved · kernel-lean · F:ml430-int-add-le-of-le-sub-left-b5bfaca2 11 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_le_of_le_sub_right proved · kernel-lean · F:ml430-int-add-le-of-le-sub-right-6cf92559 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_left_cancel proved · kernel-lean · F:ml430-int-add-left-cancel-eca3a10d 4 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.add_left_comm proved · kernel-lean · F:ml430-int-add-left-comm-519fffa6 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_left_inj proved · kernel-lean · F:ml430-int-add-left-inj-befcca48 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_left_neg proved · kernel-lean · F:ml430-int-add-left-neg-c1bf80e1 2 dependencies
5 dependents
-
Mathlib v4.30 source proposition Int.add_modEq_left proved · kernel-lean · F:ml430-int-add-modeq-left-ee732b5b 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_modEq_right proved · kernel-lean · F:ml430-int-add-modeq-right-e58108ee 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_mul proved · kernel-lean · F:ml430-int-add-mul-66aa025b 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.add_mul_ediv_left open · route not assigned · F:ml430-int-add-mul-ediv-left-3f1150d1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_mul_ediv_right open · route not assigned · F:ml430-int-add-mul-ediv-right-edd6fbac 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_neg_cancel_left proved · kernel-lean · F:ml430-int-add-neg-cancel-left-580f2be4 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_neg_cancel_right proved · kernel-lean · F:ml430-int-add-neg-cancel-right-98f97323 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_neg_eq_sub proved · kernel-lean · F:ml430-int-add-neg-eq-sub-32f34729 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.add_one_ediv_two_mul_two_of_odd proved · kernel-lean · F:ml430-int-add-one-ediv-two-mul-two-of-odd-3c9ef32f 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_one_le_of_not_le open · route not assigned · F:ml430-int-add-one-le-of-not-le-fd7eda8b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.add_two_le_iff_lt_of_even_sub open · route not assigned · F:ml430-int-add-two-le-iff-lt-of-even-sub-5f816323 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_dvd_iff_dvd_mul open · route not assigned · F:ml430-int-div-dvd-iff-dvd-mul-a8c3badc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_div_iff_of_dvd_of_neg_of_neg open · route not assigned · F:ml430-int-div-le-div-iff-of-dvd-of-neg-of-neg-2a406b84 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_div_iff_of_dvd_of_neg_of_pos open · route not assigned · F:ml430-int-div-le-div-iff-of-dvd-of-neg-of-pos-9c8d8a09 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_div_iff_of_dvd_of_pos_of_neg open · route not assigned · F:ml430-int-div-le-div-iff-of-dvd-of-pos-of-neg-9de4290e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_div_iff_of_dvd_of_pos_of_pos open · route not assigned · F:ml430-int-div-le-div-iff-of-dvd-of-pos-of-pos-ae84c83e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_iff_of_dvd_of_neg open · route not assigned · F:ml430-int-div-le-iff-of-dvd-of-neg-56f5d86e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_le_iff_of_dvd_of_pos open · route not assigned · F:ml430-int-div-le-iff-of-dvd-of-pos-d6e9563a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_lt_div_iff_of_dvd_of_neg_of_neg open · route not assigned · F:ml430-int-div-lt-div-iff-of-dvd-of-neg-of-neg-aaf3dbfe 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_lt_div_iff_of_dvd_of_neg_of_pos open · route not assigned · F:ml430-int-div-lt-div-iff-of-dvd-of-neg-of-pos-f131fc0e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.div_lt_div_iff_of_dvd_of_pos open · route not assigned · F:ml430-int-div-lt-div-iff-of-dvd-of-pos-a3d09d53 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_coe_gcd proved · kernel-lean · F:ml430-int-dvd-coe-gcd-6bda035e 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_coe_gcd_iff proved · kernel-lean · F:ml430-int-dvd-coe-gcd-iff-143eb02f 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_emod_add_of_dvd_add open · route not assigned · F:ml430-int-dvd-emod-add-of-dvd-add-3d3b6f29 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_gcd proved · kernel-lean · F:ml430-int-dvd-gcd-aebc8aa1 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_gcd_iff proved · kernel-lean · F:ml430-int-dvd-gcd-iff-5c30733d 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_gcd_mul_gcd_iff_dvd_mul proved · kernel-lean · F:ml430-int-dvd-gcd-mul-gcd-iff-dvd-mul-8ea752a5 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_gcd_mul_iff_dvd_mul proved · kernel-lean · F:ml430-int-dvd-gcd-mul-iff-dvd-mul-12f61b99 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_mul proved · kernel-lean · F:ml430-int-dvd-mul-3a7b94cd 18 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_mul_emod_add_of_dvd_mul_add open · route not assigned · F:ml430-int-dvd-mul-emod-add-of-dvd-mul-add-8a4f82e3 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_mul_gcd_iff_dvd_mul proved · kernel-lean · F:ml430-int-dvd-mul-gcd-iff-dvd-mul-22d6488e 5 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.dvd_natCast open · route not assigned · F:ml430-int-dvd-natcast-84ee4207 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_of_dvd_mul_left_of_gcd_one proved · kernel-lean · F:ml430-int-dvd-of-dvd-mul-left-of-gcd-one-649e349b 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.dvd_of_dvd_mul_right_of_gcd_one proved · kernel-lean · F:ml430-int-dvd-of-dvd-mul-right-of-gcd-one-77817ff0 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.dvd_of_mul_dvd open · route not assigned · F:ml430-int-dvd-of-mul-dvd-c09d49d1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ediv_gcd_ne_zero_if_ne_zero_right proved · kernel-lean · F:ml430-int-ediv-gcd-ne-zero-if-ne-zero-right-e1bda815 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ediv_gcd_ne_zero_of_ne_zero_left proved · kernel-lean · F:ml430-int-ediv-gcd-ne-zero-of-ne-zero-left-2778814c 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ediv_two_mul_two_add_one_of_odd proved · kernel-lean · F:ml430-int-ediv-two-mul-two-add-one-of-odd-a7ec30d7 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ediv_two_mul_two_of_even proved · kernel-lean · F:ml430-int-ediv-two-mul-two-of-even-0095e2a6 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.emod_eq_sub_self_emod open · route not assigned · F:ml430-int-emod-eq-sub-self-emod-8ceed103 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.emod_two_ne_one proved · kernel-lean · F:ml430-int-emod-two-ne-one-5b930333 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.emod_two_ne_zero proved · kernel-lean · F:ml430-int-emod-two-ne-zero-d07d008f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_natCast_toNat open · route not assigned · F:ml430-int-eq-natcast-tonat-0270a7b2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs open · route not assigned · F:ml430-int-eq-of-mod-eq-of-natabs-sub-lt-natabs-67e7052a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_of_mul_eq_one open · route not assigned · F:ml430-int-eq-of-mul-eq-one-0e6b8782 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_one_or_neg_one_of_mul_eq_neg_one open · route not assigned · F:ml430-int-eq-one-or-neg-one-of-mul-eq-neg-one-b8df542e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_one_or_neg_one_of_mul_eq_neg_one' open · route not assigned · F:ml430-int-eq-one-or-neg-one-of-mul-eq-neg-one-be9181e7 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_one_or_neg_one_of_mul_eq_one open · route not assigned · F:ml430-int-eq-one-or-neg-one-of-mul-eq-one-79096e09 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_one_or_neg_one_of_mul_eq_one' open · route not assigned · F:ml430-int-eq-one-or-neg-one-of-mul-eq-one-9cbac9dc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_zero_of_dvd_of_nonneg_of_lt open · route not assigned · F:ml430-int-eq-zero-of-dvd-of-nonneg-of-lt-87fe63a0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.eq_zero_or_eq_zero_of_mul_eq_zero proved · kernel-lean · F:ml430-int-eq-zero-or-eq-zero-of-mul-eq-zero-da702fe4 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.even_add proved · kernel-lean · F:ml430-int-even-add-3c4536e3 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.even_add' proved · kernel-lean · F:ml430-int-even-add-bc8e1394 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.even_add_one proved · kernel-lean · F:ml430-int-even-add-one-af33da18 8 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.exists_gcd_one' proved · kernel-lean · F:ml430-int-exists-gcd-one-657db3e2 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.exists_gcd_one proved · kernel-lean · F:ml430-int-exists-gcd-one-d8820780 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.exists_greatest_of_bdd open · route not assigned · F:ml430-int-exists-greatest-of-bdd-540c90cf 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.exists_least_of_bdd open · route not assigned · F:ml430-int-exists-least-of-bdd-5b2bde8b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_add proved · kernel-lean · F:ml430-int-fib-add-181b6a2c 9 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.fib_add_one proved · kernel-lean · F:ml430-int-fib-add-one-33f1b748 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_add_two proved · kernel-lean · F:ml430-int-fib-add-two-739358dd 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.fib_dvd proved · kernel-lean · F:ml430-int-fib-dvd-ffb3c5c1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_eq_fib_add_two_sub_fib_add_one proved · kernel-lean · F:ml430-int-fib-eq-fib-add-two-sub-fib-add-one-0dab3f6d 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_eq_zero proved · kernel-lean · F:ml430-int-fib-eq-zero-8193c7cb 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_gcd proved · kernel-lean · F:ml430-int-fib-gcd-3a8bfdec 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_natCast proved · kernel-lean · F:ml430-int-fib-natcast-d5886be4 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.fib_neg proved · kernel-lean · F:ml430-int-fib-neg-b4021d37 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.fib_neg_one proved · kernel-lean · F:ml430-int-fib-neg-one-107bdfc6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_neg_two proved · kernel-lean · F:ml430-int-fib-neg-two-379ecfa0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_of_nonneg proved · kernel-lean · F:ml430-int-fib-of-nonneg-438018c5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_of_odd proved · kernel-lean · F:ml430-int-fib-of-odd-66560495 10 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.fib_one proved · kernel-lean · F:ml430-int-fib-one-df6c44d8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_two proved · kernel-lean · F:ml430-int-fib-two-33d76423 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_two_mul proved · kernel-lean · F:ml430-int-fib-two-mul-0e70f3dd 9 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.fib_two_mul_add_one_eq_natFib_natAbs proved · kernel-lean · F:ml430-int-fib-two-mul-add-one-eq-natfib-natabs-61a8342b 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_two_mul_add_one_pos proved · kernel-lean · F:ml430-int-fib-two-mul-add-one-pos-8977f65f 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_two_mul_add_two proved · kernel-lean · F:ml430-int-fib-two-mul-add-two-0ba4a948 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.fib_zero proved · kernel-lean · F:ml430-int-fib-zero-439bfeee 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_div proved · kernel-lean · F:ml430-int-gcd-div-5e01872f 26 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_div_gcd_div_gcd proved · kernel-lean · F:ml430-int-gcd-div-gcd-div-gcd-2db608dc 16 dependencies
3 dependents
-
Mathlib v4.30 source proposition Int.gcd_dvd_iff proved · kernel-lean · F:ml430-int-gcd-dvd-iff-66fa03b3 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_emod open · route not assigned · F:ml430-int-gcd-emod-66050e90 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_eq_gcd_ab proved · kernel-lean · F:ml430-int-gcd-eq-gcd-ab-63005aef 4 dependencies
4 dependents
-
Mathlib v4.30 source proposition Int.gcd_eq_one_of_gcd_mul_right_eq_one_left proved · kernel-lean · F:ml430-int-gcd-eq-one-of-gcd-mul-right-eq-one-left-8533eb82 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_eq_one_of_gcd_mul_right_eq_one_right proved · kernel-lean · F:ml430-int-gcd-eq-one-of-gcd-mul-right-eq-one-right-a9b19222 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_fib proved · kernel-lean · F:ml430-int-gcd-fib-73bdafc2 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.gcd_greatest proved · kernel-lean · F:ml430-int-gcd-greatest-5b31c5fe 11 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.gcd_ne_one_iff_gcd_mul_right_ne_one proved · kernel-lean · F:ml430-int-gcd-ne-one-iff-gcd-mul-right-ne-one-ae6099bd 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_rcc_left open · route not assigned · F:ml430-int-induct-rcc-left-b1583f11 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_rcc_right open · route not assigned · F:ml430-int-induct-rcc-right-5d3f1a22 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_rco_left open · route not assigned · F:ml430-int-induct-rco-left-44aea79a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_rco_right open · route not assigned · F:ml430-int-induct-rco-right-f62a54c5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_roc_left open · route not assigned · F:ml430-int-induct-roc-left-ba1f9783 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_roc_right open · route not assigned · F:ml430-int-induct-roc-right-0f595642 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_roo_left open · route not assigned · F:ml430-int-induct-roo-left-c3e749b7 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.induct_roo_right open · route not assigned · F:ml430-int-induct-roo-right-5c8bce01 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.le.elim proved · kernel-lean · F:ml430-int-le-elim-efa70bfa 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.le_of_ofNat_le_ofNat proved · kernel-lean · F:ml430-int-le-of-ofnat-le-ofnat-483e0f18 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.le_sub_one_of_not_le open · route not assigned · F:ml430-int-le-sub-one-of-not-le-fc32b89d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt.elim proved · kernel-lean · F:ml430-int-lt-elim-35b9d0f8 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt_of_ofNat_lt_ofNat proved · kernel-lean · F:ml430-int-lt-of-ofnat-lt-ofnat-968e5a43 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt_of_sum_four_squares_eq_mul open · route not assigned · F:ml430-int-lt-of-sum-four-squares-eq-mul-449dddb6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt_of_toNat_lt open · route not assigned · F:ml430-int-lt-of-tonat-lt-0b04114f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt_or_eq_of_le open · route not assigned · F:ml430-int-lt-or-eq-of-le-28b5d4e8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.lt_toNat open · route not assigned · F:ml430-int-lt-tonat-18a10163 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mod_modEq proved · kernel-lean · F:ml430-int-mod-modeq-6bec7847 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add proved · kernel-lean · F:ml430-int-modeq-add-b805125a 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_left proved · kernel-lean · F:ml430-int-modeq-add-left-6e17c69a 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_left_cancel' proved · kernel-lean · F:ml430-int-modeq-add-left-cancel-062ad5fe 5 dependencies
3 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_left_cancel proved · kernel-lean · F:ml430-int-modeq-add-left-cancel-c1adde5a 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_right_cancel proved · kernel-lean · F:ml430-int-modeq-add-right-cancel-d7366811 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_right_cancel' proved · kernel-lean · F:ml430-int-modeq-add-right-cancel-f74acb64 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.ModEq.add_right proved · kernel-lean · F:ml430-int-modeq-add-right-fa8f7abe 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.cancel_left_div_gcd proved · kernel-lean · F:ml430-int-modeq-cancel-left-div-gcd-b2d407e8 24 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.ModEq.cancel_right_div_gcd proved · kernel-lean · F:ml430-int-modeq-cancel-right-div-gcd-00cd73fa 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.modEq_comm proved · kernel-lean · F:ml430-int-modeq-comm-1e4bcc07 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.dvd proved · kernel-lean · F:ml430-int-modeq-dvd-1ce6b46e 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.dvd_iff proved · kernel-lean · F:ml430-int-modeq-dvd-iff-b7ffeff8 11 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.eq proved · kernel-lean · F:ml430-int-modeq-eq-696e85f7 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.mul proved · kernel-lean · F:ml430-int-modeq-mul-6736aa2e 14 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.modEq_neg proved · kernel-lean · F:ml430-int-modeq-neg-d6ff57b6 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.ModEq.neg proved · kernel-lean · F:ml430-int-modeq-neg-f649f6c5 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.ModEq.of_dvd proved · kernel-lean · F:ml430-int-modeq-of-dvd-b9c41fce 10 dependencies
2 dependents
-
Mathlib v4.30 source proposition Int.ModEq.of_mul_left proved · kernel-lean · F:ml430-int-modeq-of-mul-left-c4ccd51e 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.ModEq.of_mul_right proved · kernel-lean · F:ml430-int-modeq-of-mul-right-c92b7bf0 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.modEq_one proved · kernel-lean · F:ml430-int-modeq-one-01d9de39 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.refl proved · kernel-lean · F:ml430-int-modeq-refl-30e15520 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.modEq_sub proved · kernel-lean · F:ml430-int-modeq-sub-3148f130 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ModEq.symm proved · kernel-lean · F:ml430-int-modeq-symm-984a6e67 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Int.ModEq.trans proved · kernel-lean · F:ml430-int-modeq-trans-6d7863e0 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.modulus_modEq_zero proved · kernel-lean · F:ml430-int-modulus-modeq-zero-5b57a898 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_ediv_le_mul_ediv_assoc open · route not assigned · F:ml430-int-mul-ediv-le-mul-ediv-assoc-114d9ea9 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_eq_neg_one_iff_eq_one_or_neg_one open · route not assigned · F:ml430-int-mul-eq-neg-one-iff-eq-one-or-neg-one-baa79d49 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_eq_one_iff_eq_one_or_neg_one open · route not assigned · F:ml430-int-mul-eq-one-iff-eq-one-or-neg-one-073ece31 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg open · route not assigned · F:ml430-int-mul-le-mul-of-le-of-le-of-nonneg-of-nonneg-5d7e65e5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonpos open · route not assigned · F:ml430-int-mul-le-mul-of-le-of-le-of-nonneg-of-nonpos-7e223ee0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonneg open · route not assigned · F:ml430-int-mul-le-mul-of-le-of-le-of-nonpos-of-nonneg-a449a2a6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonpos open · route not assigned · F:ml430-int-mul-le-mul-of-le-of-le-of-nonpos-of-nonpos-7980025b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_le_mul_of_natAbs_le open · route not assigned · F:ml430-int-mul-le-mul-of-natabs-le-e87cd800 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_neg_iff proved · kernel-lean · F:ml430-int-mul-neg-iff-79c18955 18 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_nonneg_iff proved · kernel-lean · F:ml430-int-mul-nonneg-iff-4a7185c1 8 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_nonneg_of_nonneg_or_nonpos proved · kernel-lean · F:ml430-int-mul-nonneg-of-nonneg-or-nonpos-79da88c9 8 dependencies
1 dependents
-
Mathlib v4.30 source proposition Int.mul_nonpos_iff proved · kernel-lean · F:ml430-int-mul-nonpos-iff-4da0d0b9 15 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.mul_pos_iff proved · kernel-lean · F:ml430-int-mul-pos-iff-e4bfa31d 17 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_coe_sub_coe_le_of_le proved · kernel-lean · F:ml430-int-natabs-coe-sub-coe-le-of-le-d2800d86 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_coe_sub_coe_lt_of_lt proved · kernel-lean · F:ml430-int-natabs-coe-sub-coe-lt-of-lt-e0566dd0 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_emod_two proved · kernel-lean · F:ml430-int-natabs-emod-two-18514063 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_eq_iff_mul_self_eq proved · kernel-lean · F:ml430-int-natabs-eq-iff-mul-self-eq-f1c49fdf 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_inj_of_nonneg_of_nonneg proved · kernel-lean · F:ml430-int-natabs-inj-of-nonneg-of-nonneg-db3f2d3d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_inj_of_nonneg_of_nonpos proved · kernel-lean · F:ml430-int-natabs-inj-of-nonneg-of-nonpos-b5d96f53 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_inj_of_nonpos_of_nonneg proved · kernel-lean · F:ml430-int-natabs-inj-of-nonpos-of-nonneg-ecdb334a 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_inj_of_nonpos_of_nonpos proved · kernel-lean · F:ml430-int-natabs-inj-of-nonpos-of-nonpos-87475bd8 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_le_iff_mul_self_le proved · kernel-lean · F:ml430-int-natabs-le-iff-mul-self-le-20242c1d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_le_of_dvd_ne_zero open · route not assigned · F:ml430-int-natabs-le-of-dvd-ne-zero-a8fcd923 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natAbs_lt_iff_mul_self_lt proved · kernel-lean · F:ml430-int-natabs-lt-iff-mul-self-lt-5f19cd1f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natCast_dvd open · route not assigned · F:ml430-int-natcast-dvd-cb62f648 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natCast_dvd_ofNat open · route not assigned · F:ml430-int-natcast-dvd-ofnat-8d8307a2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natCast_ediv open · route not assigned · F:ml430-int-natcast-ediv-2b4e8324 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natCast_inj open · route not assigned · F:ml430-int-natcast-inj-9dc3b9c2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.natCast_le_zero open · route not assigned · F:ml430-int-natcast-le-zero-bfce410a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ne_zero_of_gcd proved · kernel-lean · F:ml430-int-ne-zero-of-gcd-f71f00df 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.neg_modEq_neg proved · kernel-lean · F:ml430-int-neg-modeq-neg-30d98479 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.negSucc_ediv_negSucc open · route not assigned · F:ml430-int-negsucc-ediv-negsucc-74a87fde 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.negSucc_ediv_ofNat_succ open · route not assigned · F:ml430-int-negsucc-ediv-ofnat-succ-27c87d32 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.not_le_eq open · route not assigned · F:ml430-int-not-le-eq-a1aa34a4 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.not_lt_eq open · route not assigned · F:ml430-int-not-lt-eq-120ae6c2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.not_prime_of_int_mul proved · kernel-lean · F:ml430-int-not-prime-of-int-mul-e3060f5d 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.Odd.of_mul_left proved · kernel-lean · F:ml430-int-odd-of-mul-left-b580971e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.Odd.of_mul_right proved · kernel-lean · F:ml430-int-odd-of-mul-right-d6d1fc1d 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ofNat_eq_coe open · route not assigned · F:ml430-int-ofnat-eq-coe-f82fca8a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ofNat_eq_natCast open · route not assigned · F:ml430-int-ofnat-eq-natcast-001cc3e2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ofNat_one open · route not assigned · F:ml430-int-ofnat-one-8ef5badc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ofNat_two open · route not assigned · F:ml430-int-ofnat-two-20e97f9e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.ofNat_zero open · route not assigned · F:ml430-int-ofnat-zero-0d364f22 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.Prime.dvd_mul' proved · kernel-lean · F:ml430-int-prime-dvd-mul-23b73e69 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.Prime.dvd_mul proved · kernel-lean · F:ml430-int-prime-dvd-mul-90351ba0 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.sq_ne_two_mod_four open · route not assigned · F:ml430-int-sq-ne-two-mod-four-3d69c9b6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul proved · kernel-lean · F:ml430-int-succ-dvd-or-succ-dvd-of-succ-sum-dvd-mul-435a4948 13 dependencies
0 dependents
-
Mathlib v4.30 source proposition Int.two_le_iff_pos_of_even open · route not assigned · F:ml430-int-two-le-iff-pos-of-even-64eb33a6 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.fib_eq_zero open · route not assigned · F:ml430-mutation-1432b2277cf2cc26c1d11cd6 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.sqrt_le_self open · route not assigned · F:ml430-mutation-2086302b3a338591b3179871 0 dependencies
0 dependents
-
Outcome-blind mutation of Int.ne_zero_of_gcd open · route not assigned · F:ml430-mutation-48fe130e2b8eadb6f626b66f 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.Prime.pred_pos open · route not assigned · F:ml430-mutation-5179f333b8333ecff8adc223 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.factorial_ne_zero open · route not assigned · F:ml430-mutation-7afa5ec620720a1501bf349d 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.lor_comm open · route not assigned · F:ml430-mutation-a6dd1759bce60d820292e107 0 dependencies
0 dependents
-
Outcome-blind mutation of Int.fib_eq_zero open · route not assigned · F:ml430-mutation-aabb80b1f89f0c5847364692 0 dependencies
0 dependents
-
Outcome-blind mutation of Int.ModEq.symm open · route not assigned · F:ml430-mutation-aca37b68d3cdf06f0127def9 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.not_coprime_zero_zero open · route not assigned · F:ml430-mutation-c20db9b4c60b816ce738bdf2 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.ModEq.symm open · route not assigned · F:ml430-mutation-c86940b52af8159ca9b381d6 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.log_le_self open · route not assigned · F:ml430-mutation-e8583599cfae2d40cefae3f0 0 dependencies
0 dependents
-
Outcome-blind mutation of Nat.choose_self open · route not assigned · F:ml430-mutation-edb05acf07d9ef3f9f8232fc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.abundant_iff_not_perfect_and_not_deficient proved · kernel-lean · F:ml430-nat-abundant-iff-not-perfect-and-not-deficient-9763e268 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Abundant.mul_left proved · kernel-lean · F:ml430-nat-abundant-mul-left-4de4fbe7 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Abundant.of_dvd proved · kernel-lean · F:ml430-nat-abundant-of-dvd-686548ce 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.abundant_twelve proved · kernel-lean · F:ml430-nat-abundant-twelve-24ce1ba6 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_add_add_comm proved · kernel-lean · F:ml430-nat-add-add-add-comm-74d2c151 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.add_assoc proved · kernel-lean · F:ml430-nat-add-assoc-8c87a1f1 0 dependencies
76 dependents
-
Mathlib v4.30 source proposition Nat.add_choose proved · kernel-lean · F:ml430-nat-add-choose-eb49fa11 8 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_choose_mul_factorial_mul_factorial proved · kernel-lean · F:ml430-nat-add-choose-mul-factorial-mul-factorial-26ba01ef 4 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_comm proved · kernel-lean · F:ml430-nat-add-comm-56a2d614 2 dependencies
159 dependents
-
Mathlib v4.30 source proposition Nat.add_descFactorial_eq_ascFactorial proved · kernel-lean · F:ml430-nat-add-descfactorial-eq-ascfactorial-5faac784 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_div_left proved · kernel-lean · F:ml430-nat-add-div-left-1b15b2b2 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_div_of_dvd_add_add_one proved · kernel-lean · F:ml430-nat-add-div-of-dvd-add-add-one-f17dffc0 22 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_div_right proved · kernel-lean · F:ml430-nat-add-div-right-4b60b393 5 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_eq proved · kernel-lean · F:ml430-nat-add-eq-ab0eab69 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_left proved · kernel-lean · F:ml430-nat-add-eq-left-8e12789f 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_max_iff proved · kernel-lean · F:ml430-nat-add-eq-max-iff-39576e6d 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_min_iff proved · kernel-lean · F:ml430-nat-add-eq-min-iff-e60cf432 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_one_iff proved · kernel-lean · F:ml430-nat-add-eq-one-iff-f8463abc 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_right proved · kernel-lean · F:ml430-nat-add-eq-right-9067eb1a 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_three_iff proved · kernel-lean · F:ml430-nat-add-eq-three-iff-799a0a8f 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_two_iff proved · kernel-lean · F:ml430-nat-add-eq-two-iff-25385c65 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_eq_zero proved · kernel-lean · F:ml430-nat-add-eq-zero-64233539 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_factorial_le_factorial_add proved · kernel-lean · F:ml430-nat-add-factorial-le-factorial-add-b0400cf6 9 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_factorial_lt_factorial_add proved · kernel-lean · F:ml430-nat-add-factorial-lt-factorial-add-7501a8c8 16 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_factorial_succ_le_factorial_add_succ proved · kernel-lean · F:ml430-nat-add-factorial-succ-le-factorial-add-succ-e8145feb 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_factorial_succ_lt_factorial_add_succ proved · kernel-lean · F:ml430-nat-add-factorial-succ-lt-factorial-add-succ-ec0fa8d3 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_le_pair open · route not assigned · F:ml430-nat-add-le-pair-4af701ca 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_max_add_left proved · kernel-lean · F:ml430-nat-add-max-add-left-37eb9f8d 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_max_add_right proved · kernel-lean · F:ml430-nat-add-max-add-right-178bc311 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_min_add_left proved · kernel-lean · F:ml430-nat-add-min-add-left-9728864e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_min_add_right proved · kernel-lean · F:ml430-nat-add-min-add-right-b483207e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_mod_left proved · kernel-lean · F:ml430-nat-add-mod-left-6b337077 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_mod_right proved · kernel-lean · F:ml430-nat-add-mod-right-c047c67a 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_modEq_left proved · kernel-lean · F:ml430-nat-add-modeq-left-e3b1fba9 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_modEq_right proved · kernel-lean · F:ml430-nat-add-modeq-right-e2f11f21 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_mul_div_left proved · kernel-lean · F:ml430-nat-add-mul-div-left-e20827dd 4 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.add_mul_div_right proved · kernel-lean · F:ml430-nat-add-mul-div-right-44a689e4 5 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_mul_lt_mul_of_lt_of_lt open · route not assigned · F:ml430-nat-add-mul-lt-mul-of-lt-of-lt-4d1d3fbc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_mul_mod_self_left proved · kernel-lean · F:ml430-nat-add-mul-mod-self-left-108b5fe0 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.add_mul_mod_self_right proved · kernel-lean · F:ml430-nat-add-mul-mod-self-right-ac5b3624 8 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_one_lt_of_even proved · kernel-lean · F:ml430-nat-add-one-lt-of-even-3464b374 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_one_mul_choose_eq proved · kernel-lean · F:ml430-nat-add-one-mul-choose-eq-d364de16 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.add_pos_right proved · kernel-lean · F:ml430-nat-add-pos-right-e43374dc 3 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.and_assoc proved · kernel-lean · F:ml430-nat-and-assoc-273b60d8 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_comm proved · kernel-lean · F:ml430-nat-and-comm-7525d05a 3 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.and_div_two proved · kernel-lean · F:ml430-nat-and-div-two-1a2f7c33 19 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_le_left proved · kernel-lean · F:ml430-nat-and-le-left-6d04acb7 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.and_le_right proved · kernel-lean · F:ml430-nat-and-le-right-a3f80076 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_mod_two_eq_one proved · kernel-lean · F:ml430-nat-and-mod-two-eq-one-3e873792 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_one_is_mod proved · kernel-lean · F:ml430-nat-and-one-is-mod-d861e96b 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_or_distrib_left proved · kernel-lean · F:ml430-nat-and-or-distrib-left-fe131f64 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_or_distrib_right proved · kernel-lean · F:ml430-nat-and-or-distrib-right-0daaa284 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.and_self proved · kernel-lean · F:ml430-nat-and-self-06a84ccc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ascFactorial_eq_div proved · kernel-lean · F:ml430-nat-ascfactorial-eq-div-87d768e8 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ascFactorial_zero proved · kernel-lean · F:ml430-nat-ascfactorial-zero-fd183202 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.avg_comm open · route not assigned · F:ml430-nat-avg-comm-7c5dd07e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.avg_le_left open · route not assigned · F:ml430-nat-avg-le-left-4a112778 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.avg_le_right open · route not assigned · F:ml430-nat-avg-le-right-9fa159da 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.avg_lt_left open · route not assigned · F:ml430-nat-avg-lt-left-14dbe48e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.avg_lt_right open · route not assigned · F:ml430-nat-avg-lt-right-e1a68d05 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.base_induction proved · kernel-lean · F:ml430-nat-base-induction-83561d4c 14 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bertrand open · route not assigned · F:ml430-nat-bertrand-d35d0477 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_add proved · kernel-lean · F:ml430-nat-bit-add-b1edcc8e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_add' proved · kernel-lean · F:ml430-nat-bit-add-d487108f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_div_two open · route not assigned · F:ml430-nat-bit-div-two-d74e7898 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_eq_zero_iff open · route not assigned · F:ml430-nat-bit-eq-zero-iff-6b701e2b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_false proved · kernel-lean · F:ml430-nat-bit-false-98b0bf2a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_false_apply proved · kernel-lean · F:ml430-nat-bit-false-apply-5962146d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_false_zero proved · kernel-lean · F:ml430-nat-bit-false-zero-d996adbf 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_le proved · kernel-lean · F:ml430-nat-bit-le-40743fa3 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_lt_bit proved · kernel-lean · F:ml430-nat-bit-lt-bit-295453cc 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_mod_two_eq_one_iff open · route not assigned · F:ml430-nat-bit-mod-two-eq-one-iff-d9b00bec 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_mod_two_eq_zero_iff open · route not assigned · F:ml430-nat-bit-mod-two-eq-zero-iff-b69a9790 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_ne_zero proved · kernel-lean · F:ml430-nat-bit-ne-zero-181bd65c 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_ne_zero_iff open · route not assigned · F:ml430-nat-bit-ne-zero-iff-d811128e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_true proved · kernel-lean · F:ml430-nat-bit-true-2456e237 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bit_true_apply proved · kernel-lean · F:ml430-nat-bit-true-apply-02338ebc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.bitwise_bit' proved · kernel-lean · F:ml430-nat-bitwise-bit-4c4b28a8 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.bitwise_comm proved · kernel-lean · F:ml430-nat-bitwise-comm-1a273bae 1 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.bitwise_swap proved · kernel-lean · F:ml430-nat-bitwise-swap-7175e90e 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.bitwise_zero open · route not assigned · F:ml430-nat-bitwise-zero-7c0e3f82 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ble_eq_true_of_le proved · kernel-lean · F:ml430-nat-ble-eq-true-of-le-5ce4ac2e 2 dependencies
29 dependents
-
Mathlib v4.30 source proposition Nat.ble_self_eq_true proved · kernel-lean · F:ml430-nat-ble-self-eq-true-839df126 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.ble_succ_eq_true proved · kernel-lean · F:ml430-nat-ble-succ-eq-true-000a69f4 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.case_strong_induction_on open · route not assigned · F:ml430-nat-case-strong-induction-on-0ec18022 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.cauchy_induction' open · route not assigned · F:ml430-nat-cauchy-induction-64736fbc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.cauchy_induction open · route not assigned · F:ml430-nat-cauchy-induction-fc316053 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.cauchy_induction_mul open · route not assigned · F:ml430-nat-cauchy-induction-mul-7c7491ec 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.cauchy_induction_two_mul open · route not assigned · F:ml430-nat-cauchy-induction-two-mul-d6a1fcd8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_eq_zero open · route not assigned · F:ml430-nat-ceilroot-eq-zero-a9d23c47 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_ne_zero open · route not assigned · F:ml430-nat-ceilroot-ne-zero-11a86167 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_one_left open · route not assigned · F:ml430-nat-ceilroot-one-left-fffb7237 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_one_right open · route not assigned · F:ml430-nat-ceilroot-one-right-e08e200c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_pow_self open · route not assigned · F:ml430-nat-ceilroot-pow-self-19e66788 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_zero_left open · route not assigned · F:ml430-nat-ceilroot-zero-left-c1253d24 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ceilRoot_zero_right open · route not assigned · F:ml430-nat-ceilroot-zero-right-697fdf9e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_eq_zero_of_lt proved · kernel-lean · F:ml430-nat-choose-eq-zero-of-lt-92ebab29 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_add proved · kernel-lean · F:ml430-nat-choose-le-add-9c463139 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_choose proved · kernel-lean · F:ml430-nat-choose-le-choose-907b5042 4 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_descFactorial open · route not assigned · F:ml430-nat-choose-le-descfactorial-67e8cc84 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_pow open · route not assigned · F:ml430-nat-choose-le-pow-75c38848 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_succ proved · kernel-lean · F:ml430-nat-choose-le-succ-62ae968b 4 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.choose_le_two_pow open · route not assigned · F:ml430-nat-choose-le-two-pow-ef6f7dcd 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_lt_descFactorial open · route not assigned · F:ml430-nat-choose-lt-descfactorial-add66985 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_lt_pow open · route not assigned · F:ml430-nat-choose-lt-pow-e5cc4f38 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_lt_two_pow open · route not assigned · F:ml430-nat-choose-lt-two-pow-233c6d67 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_middle_le_pow open · route not assigned · F:ml430-nat-choose-middle-le-pow-de15c8ab 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_mono proved · kernel-lean · F:ml430-nat-choose-mono-a1af9c18 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_ne_zero proved · kernel-lean · F:ml430-nat-choose-ne-zero-49c3d3cb 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_one_right proved · kernel-lean · F:ml430-nat-choose-one-right-7eda8e39 6 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.choose_self proved · kernel-lean · F:ml430-nat-choose-self-25bb9fb8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_succ_self proved · kernel-lean · F:ml430-nat-choose-succ-self-e396f6c2 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_succ_succ proved · kernel-lean · F:ml430-nat-choose-succ-succ-671856b6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_symm_add proved · kernel-lean · F:ml430-nat-choose-symm-add-e4b68161 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.choose_symm_of_eq_add proved · kernel-lean · F:ml430-nat-choose-symm-of-eq-add-9b5f9a20 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.choose_zero_right proved · kernel-lean · F:ml430-nat-choose-zero-right-1ed2802a 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.choose_zero_succ proved · kernel-lean · F:ml430-nat-choose-zero-succ-62c6520b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_anti_left proved · kernel-lean · F:ml430-nat-clog-anti-left-d72bd6cd 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_antitone_left proved · kernel-lean · F:ml430-nat-clog-antitone-left-44a87771 1 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.clog_eq_one proved · kernel-lean · F:ml430-nat-clog-eq-one-f7834503 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_mono proved · kernel-lean · F:ml430-nat-clog-mono-74b44081 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_mono_right proved · kernel-lean · F:ml430-nat-clog-mono-right-8d87a410 0 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.clog_monotone proved · kernel-lean · F:ml430-nat-clog-monotone-48fe50c6 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_of_left_le_one proved · kernel-lean · F:ml430-nat-clog-of-left-le-one-a6640cee 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_of_right_le_one proved · kernel-lean · F:ml430-nat-clog-of-right-le-one-8f11b62f 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_one_left proved · kernel-lean · F:ml430-nat-clog-one-left-b496af12 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.clog_one_right proved · kernel-lean · F:ml430-nat-clog-one-right-1ce3d52f 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.clog_pos proved · kernel-lean · F:ml430-nat-clog-pos-00852cb8 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.clog_zero_left proved · kernel-lean · F:ml430-nat-clog-zero-left-1c61a5bf 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.clog_zero_right proved · kernel-lean · F:ml430-nat-clog-zero-right-d42d47b1 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.coprime_add_self_left proved · kernel-lean · F:ml430-nat-coprime-add-self-left-5e93448c 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.coprime_add_self_right proved · kernel-lean · F:ml430-nat-coprime-add-self-right-c3ed0f45 C:greatest-common-divisor 12 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_div_left proved · kernel-lean · F:ml430-nat-coprime-coprime-div-left-6f7082bd 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_div_right proved · kernel-lean · F:ml430-nat-coprime-coprime-div-right-7a8ce438 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_dvd_left proved · kernel-lean · F:ml430-nat-coprime-coprime-dvd-left-2ce391d2 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_dvd_right proved · kernel-lean · F:ml430-nat-coprime-coprime-dvd-right-4a2670ae 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_mul_left proved · kernel-lean · F:ml430-nat-coprime-coprime-mul-left-fb5bd11a 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_mul_left_right proved · kernel-lean · F:ml430-nat-coprime-coprime-mul-left-right-910d7d8f 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_mul_right proved · kernel-lean · F:ml430-nat-coprime-coprime-mul-right-70e4e946 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.coprime_mul_right_right proved · kernel-lean · F:ml430-nat-coprime-coprime-mul-right-right-9599ecd3 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.dvd_mul_left proved · kernel-lean · F:ml430-nat-coprime-dvd-mul-left-e799d04c 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.dvd_mul_right proved · kernel-lean · F:ml430-nat-coprime-dvd-mul-right-7cd1c3c8 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.dvd_of_dvd_mul_left proved · kernel-lean · F:ml430-nat-coprime-dvd-of-dvd-mul-left-b0608cb9 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.dvd_of_dvd_mul_right proved · kernel-lean · F:ml430-nat-coprime-dvd-of-dvd-mul-right-efc3a4ec 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.eq_of_mul_eq_zero proved · kernel-lean · F:ml430-nat-coprime-eq-of-mul-eq-zero-a2026bd5 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_factorizationLCMLeft_factorizationLCMRight open · route not assigned · F:ml430-nat-coprime-factorizationlcmleft-factorizationlcmright-e7db70ce 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_fermatNumber_fermatNumber proved · kernel-lean · F:ml430-nat-coprime-fermatnumber-fermatnumber-161e79c7 23 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_iff_isRelPrime proved · kernel-lean · F:ml430-nat-coprime-iff-isrelprime-0c08eb25 C:coprime-integers 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.lcm_eq_mul proved · kernel-lean · F:ml430-nat-coprime-lcm-eq-mul-edf52888 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.mul_add_mul_ne_mul proved · kernel-lean · F:ml430-nat-coprime-mul-add-mul-ne-mul-51b56f70 21 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.odd_of_left proved · kernel-lean · F:ml430-nat-coprime-odd-of-left-ed80ab44 1 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.odd_of_right proved · kernel-lean · F:ml430-nat-coprime-odd-of-right-8dc1decc 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.of_dvd proved · kernel-lean · F:ml430-nat-coprime-of-dvd-18fcd09f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_of_dvd' proved · kernel-lean · F:ml430-nat-coprime-of-dvd-6f652673 19 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.of_dvd_left proved · kernel-lean · F:ml430-nat-coprime-of-dvd-left-b0e2aa94 C:greatest-common-divisorC:divisibility 6 dependencies
5 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.of_dvd_right proved · kernel-lean · F:ml430-nat-coprime-of-dvd-right-a640bd56 C:greatest-common-divisorC:divisibility 6 dependencies
7 dependents
-
Mathlib v4.30 source proposition Nat.coprime_of_lt_minFac open · route not assigned · F:ml430-nat-coprime-of-lt-minfac-0f79bdba 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_of_lt_prime proved · kernel-lean · F:ml430-nat-coprime-of-lt-prime-1978a919 6 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.coprime_one_left_iff proved · kernel-lean · F:ml430-nat-coprime-one-left-iff-45945e80 2 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.coprime_one_right_iff proved · kernel-lean · F:ml430-nat-coprime-one-right-iff-42fed4ce 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.coprime_or_dvd_of_prime proved · kernel-lean · F:ml430-nat-coprime-or-dvd-of-prime-65f47114 4 dependencies
6 dependents
-
Mathlib v4.30 source proposition Nat.coprime_primes proved · kernel-lean · F:ml430-nat-coprime-primes-5769049f 6 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.coprime_self_add_left proved · kernel-lean · F:ml430-nat-coprime-self-add-left-51351fa1 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.coprime_self_add_right proved · kernel-lean · F:ml430-nat-coprime-self-add-right-966e5434 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Coprime.symmetric proved · kernel-lean · F:ml430-nat-coprime-symmetric-9b5cfa12 6 dependencies
10 dependents
-
Mathlib v4.30 source proposition Nat.coprime_two_left proved · kernel-lean · F:ml430-nat-coprime-two-left-1b47e7c4 10 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.coprime_two_right proved · kernel-lean · F:ml430-nat-coprime-two-right-7c5a1850 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.deficient_iff_not_abundant_and_not_perfect proved · kernel-lean · F:ml430-nat-deficient-iff-not-abundant-and-not-perfect-18bbe30a 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.deficient_one proved · kernel-lean · F:ml430-nat-deficient-one-75f44529 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.descFactorial_le proved · kernel-lean · F:ml430-nat-descfactorial-le-2b8cc09a 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.descFactorial_of_lt proved · kernel-lean · F:ml430-nat-descfactorial-of-lt-fbcf5d26 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.descFactorial_one proved · kernel-lean · F:ml430-nat-descfactorial-one-d4856d4a 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.descFactorial_self proved · kernel-lean · F:ml430-nat-descfactorial-self-899fc0e0 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.descFactorial_zero proved · kernel-lean · F:ml430-nat-descfactorial-zero-966b01df 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.diag_induction open · route not assigned · F:ml430-nat-diag-induction-12c954e8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_add_add_left proved · kernel-lean · F:ml430-nat-dist-add-add-left-92fa4403 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.dist_add_add_right proved · kernel-lean · F:ml430-nat-dist-add-add-right-6e5d8bbb 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_comm proved · kernel-lean · F:ml430-nat-dist-comm-1fa29a04 1 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.dist_eq_intro proved · kernel-lean · F:ml430-nat-dist-eq-intro-294b44ad 8 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_eq_zero proved · kernel-lean · F:ml430-nat-dist-eq-zero-5ae5b706 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_mul_left proved · kernel-lean · F:ml430-nat-dist-mul-left-92624d63 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.dist_mul_right proved · kernel-lean · F:ml430-nat-dist-mul-right-d4e0c33d 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_pos_of_ne proved · kernel-lean · F:ml430-nat-dist-pos-of-ne-00f5e22f 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dist_self proved · kernel-lean · F:ml430-nat-dist-self-0cfa5426 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.dist.triangle_inequality proved · kernel-lean · F:ml430-nat-dist-triangle-inequality-b35e82d3 12 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_dvd_div_left proved · kernel-lean · F:ml430-nat-div-dvd-div-left-b56f6f7c 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_gcd_pos_of_pos_left proved · kernel-lean · F:ml430-nat-div-gcd-pos-of-pos-left-dd878a3f 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_gcd_pos_of_pos_right proved · kernel-lean · F:ml430-nat-div-gcd-pos-of-pos-right-8d26808c 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_lt_of_lt_mul proved · kernel-lean · F:ml430-nat-div-lt-of-lt-mul-818dc4c7 4 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.div_lt_self' open · route not assigned · F:ml430-nat-div-lt-self-4c19ff1c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_mul_cancel proved · kernel-lean · F:ml430-nat-div-mul-cancel-99799a00 6 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.div_right_comm open · route not assigned · F:ml430-nat-div-right-comm-ab79d5f8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_two_mul_two_add_one_of_odd proved · kernel-lean · F:ml430-nat-div-two-mul-two-add-one-of-odd-9e3e8b82 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.div_two_mul_two_of_even proved · kernel-lean · F:ml430-nat-div-two-mul-two-of-even-9ccc5340 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_base_mul open · route not assigned · F:ml430-nat-divmaxpow-base-mul-63c19e29 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_one_left open · route not assigned · F:ml430-nat-divmaxpow-one-left-2e311f8c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_one_right open · route not assigned · F:ml430-nat-divmaxpow-one-right-4696cbec 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_self open · route not assigned · F:ml430-nat-divmaxpow-self-19761ae0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_zero_left open · route not assigned · F:ml430-nat-divmaxpow-zero-left-8f1e9599 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.divMaxPow_zero_right open · route not assigned · F:ml430-nat-divmaxpow-zero-right-b1dfd200 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_add proved · kernel-lean · F:ml430-nat-dvd-add-0c5bcc91 1 dependencies
11 dependents
-
Mathlib v4.30 source proposition Nat.dvd_add_iff_left proved · kernel-lean · F:ml430-nat-dvd-add-iff-left-332cbe04 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.dvd_add_iff_right proved · kernel-lean · F:ml430-nat-dvd-add-iff-right-bf79c0cd 3 dependencies
6 dependents
-
Mathlib v4.30 source proposition Nat.dvd_add_self_left open · route not assigned · F:ml430-nat-dvd-add-self-left-5568ca79 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_add_self_right open · route not assigned · F:ml430-nat-dvd-add-self-right-5220f882 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_antisymm proved · kernel-lean · F:ml430-nat-dvd-antisymm-507f9026 5 dependencies
8 dependents
-
Mathlib v4.30 source proposition Nat.dvd_ceilRoot_pow open · route not assigned · F:ml430-nat-dvd-ceilroot-pow-80ce502a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Dvd.dvd.nat_lcm_left proved · kernel-lean · F:ml430-nat-dvd-dvd-nat-lcm-left-6143311e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Dvd.dvd.nat_lcm_right proved · kernel-lean · F:ml430-nat-dvd-dvd-nat-lcm-right-d05db50b 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_gcd proved · kernel-lean · F:ml430-nat-dvd-gcd-e5184fc5 6 dependencies
24 dependents
-
Mathlib v4.30 source proposition Nat.dvd_gcd_iff proved · kernel-lean · F:ml430-nat-dvd-gcd-iff-b8485987 4 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.dvd_gcd_mul_gcd_iff_dvd_mul proved · kernel-lean · F:ml430-nat-dvd-gcd-mul-gcd-iff-dvd-mul-07fec722 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_gcd_mul_iff_dvd_mul proved · kernel-lean · F:ml430-nat-dvd-gcd-mul-iff-dvd-mul-0afe640a 2 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.dvd_iff_mod_eq_zero proved · kernel-lean · F:ml430-nat-dvd-iff-mod-eq-zero-d795bfff 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_iff_prime_pow_dvd_dvd open · route not assigned · F:ml430-nat-dvd-iff-prime-pow-dvd-dvd-4458751e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_lcm_left proved · kernel-lean · F:ml430-nat-dvd-lcm-left-c83bcebc 13 dependencies
8 dependents
-
Mathlib v4.30 source proposition Nat.dvd_lcm_of_dvd_left proved · kernel-lean · F:ml430-nat-dvd-lcm-of-dvd-left-141a64bb 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_lcm_of_dvd_right proved · kernel-lean · F:ml430-nat-dvd-lcm-of-dvd-right-61a50fc3 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_lcm_right proved · kernel-lean · F:ml430-nat-dvd-lcm-right-18ab8e2f 12 dependencies
8 dependents
-
Mathlib v4.30 source proposition Nat.dvd_left_iff_eq open · route not assigned · F:ml430-nat-dvd-left-iff-eq-b9d7bb6d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mod_iff proved · kernel-lean · F:ml430-nat-dvd-mod-iff-2d082f10 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mul proved · kernel-lean · F:ml430-nat-dvd-mul-ebd102e2 15 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mul_gcd_iff_dvd_mul proved · kernel-lean · F:ml430-nat-dvd-mul-gcd-iff-dvd-mul-f9517e6b 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mul_left proved · kernel-lean · F:ml430-nat-dvd-mul-left-a1a8a4b8 2 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mul_left_of_dvd proved · kernel-lean · F:ml430-nat-dvd-mul-left-of-dvd-200e20a4 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.dvd_mul_right proved · kernel-lean · F:ml430-nat-dvd-mul-right-a87a83c4 0 dependencies
43 dependents
-
Mathlib v4.30 source proposition Nat.dvd_of_forall_prime_mul_dvd proved · kernel-lean · F:ml430-nat-dvd-of-forall-prime-mul-dvd-5898723b C:divisibilityC:prime-number 19 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_of_lcm_left_dvd proved · kernel-lean · F:ml430-nat-dvd-of-lcm-left-dvd-d6b2407c 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_of_lcm_right_dvd proved · kernel-lean · F:ml430-nat-dvd-of-lcm-right-dvd-61bd1a60 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_pow_iff_ceilRoot_dvd open · route not assigned · F:ml430-nat-dvd-pow-iff-ceilroot-dvd-f00c5188 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_right_iff_eq open · route not assigned · F:ml430-nat-dvd-right-iff-eq-4ce70bc6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.dvd_two_of_totient_le_one proved · kernel-lean · F:ml430-nat-dvd-two-of-totient-le-one-3642bf31 17 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.eq_of_beq_eq_true proved · kernel-lean · F:ml430-nat-eq-of-beq-eq-true-6ec35ee4 0 dependencies
26 dependents
-
Mathlib v4.30 source proposition Nat.eq_or_eq_of_totient_eq_totient proved · kernel-lean · F:ml430-nat-eq-or-eq-of-totient-eq-totient-d4d154c7 C:eulers-totient-functionC:divisibility 13 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.eq_zero_of_gcd_eq_zero_left proved · kernel-lean · F:ml430-nat-eq-zero-of-gcd-eq-zero-left-72cc4246 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.eq_zero_of_gcd_eq_zero_right proved · kernel-lean · F:ml430-nat-eq-zero-of-gcd-eq-zero-right-24054a86 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.eq_zero_of_lcm_eq_zero proved · kernel-lean · F:ml430-nat-eq-zero-of-lcm-eq-zero-d09b7af7 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.euler_four_squares open · route not assigned · F:ml430-nat-euler-four-squares-21d8c900 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.even_add proved · kernel-lean · F:ml430-nat-even-add-31386639 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.even_add' proved · kernel-lean · F:ml430-nat-even-add-39e3bc07 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.even_add_one proved · kernel-lean · F:ml430-nat-even-add-one-15b5cb18 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.even_div proved · kernel-lean · F:ml430-nat-even-div-395c6b5e 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.even_iff proved · kernel-lean · F:ml430-nat-even-iff-024826e9 7 dependencies
14 dependents
-
Mathlib v4.30 source proposition Nat.even_xor proved · kernel-lean · F:ml430-nat-even-xor-78a39432 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le open · route not assigned · F:ml430-nat-exists-add-mul-eq-of-gcd-dvd-of-mul-pred-le-e4a87d78 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_eq_pow_mul_and_not_dvd open · route not assigned · F:ml430-nat-exists-eq-pow-mul-and-not-dvd-ea40a197 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow open · route not assigned · F:ml430-nat-exists-eq-pow-of-exponent-coprime-of-pow-eq-pow-17408247 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_eq_pow_of_pow_eq_pow open · route not assigned · F:ml430-nat-exists-eq-pow-of-pow-eq-pow-127883b7 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_eq_two_pow_mul_odd open · route not assigned · F:ml430-nat-exists-eq-two-pow-mul-odd-e7310d1c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_mul_mod_eq_gcd proved · kernel-lean · F:ml430-nat-exists-mul-mod-eq-gcd-8bf9ec7e 15 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_mul_self open · route not assigned · F:ml430-nat-exists-mul-self-e73ca9fa 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_not_and_succ_of_not_zero_of_exists open · route not assigned · F:ml430-nat-exists-not-and-succ-of-not-zero-of-exists-07952ae8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_pow_eq_iff' open · route not assigned · F:ml430-nat-exists-pow-eq-iff-b8198130 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_pow_eq_iff open · route not assigned · F:ml430-nat-exists-pow-eq-iff-f581ca30 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_prime_lt_and_le_two_mul open · route not assigned · F:ml430-nat-exists-prime-lt-and-le-two-mul-a80e6056 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_prime_lt_and_le_two_mul_eventually open · route not assigned · F:ml430-nat-exists-prime-lt-and-le-two-mul-eventually-5743fe5b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.exists_prime_lt_and_le_two_mul_succ open · route not assigned · F:ml430-nat-exists-prime-lt-and-le-two-mul-succ-0c2eec3c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorial_dvd_ascFactorial proved · kernel-lean · F:ml430-nat-factorial-dvd-ascfactorial-44a4e641 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorial_dvd_descFactorial proved · kernel-lean · F:ml430-nat-factorial-dvd-descfactorial-bbf6124f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorial_dvd_factorial proved · kernel-lean · F:ml430-nat-factorial-dvd-factorial-e9d14845 6 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.factorial_le proved · kernel-lean · F:ml430-nat-factorial-le-d0f4a912 4 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.factorial_lt_of_lt proved · kernel-lean · F:ml430-nat-factorial-lt-of-lt-d6c2125d 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.factorial_ne_zero proved · kernel-lean · F:ml430-nat-factorial-ne-zero-5fc0b0a1 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorial_pos proved · kernel-lean · F:ml430-nat-factorial-pos-f1dd2405 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMLeft_dvd_left open · route not assigned · F:ml430-nat-factorizationlcmleft-dvd-left-324f9e3c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMLeft_mul_factorizationLCMRight open · route not assigned · F:ml430-nat-factorizationlcmleft-mul-factorizationlcmright-0689efd5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMLeft_pos open · route not assigned · F:ml430-nat-factorizationlcmleft-pos-820998f6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMLeft_zero_left open · route not assigned · F:ml430-nat-factorizationlcmleft-zero-left-ea02654b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMLeft_zero_right open · route not assigned · F:ml430-nat-factorizationlcmleft-zero-right-e1f61ad0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMRight_dvd_right open · route not assigned · F:ml430-nat-factorizationlcmright-dvd-right-2460f9fd 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMRight_pos open · route not assigned · F:ml430-nat-factorizationlcmright-pos-dc3f4b60 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCMRight_zero_right open · route not assigned · F:ml430-nat-factorizationlcmright-zero-right-3f1474ee 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.factorizationLCRight_zero_left open · route not assigned · F:ml430-nat-factorizationlcright-zero-left-ef4c6211 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fastFib_eq open · route not assigned · F:ml430-nat-fastfib-eq-cde11774 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermat_primeFactors_one_lt open · route not assigned · F:ml430-nat-fermat-primefactors-one-lt-58343c6f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_mono proved · kernel-lean · F:ml430-nat-fermatnumber-mono-b051cee6 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_ne_one proved · kernel-lean · F:ml430-nat-fermatnumber-ne-one-91232d67 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_one proved · kernel-lean · F:ml430-nat-fermatnumber-one-b1b0798f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_strictMono proved · kernel-lean · F:ml430-nat-fermatnumber-strictmono-acbcb8c6 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_two proved · kernel-lean · F:ml430-nat-fermatnumber-two-3aa3bfc4 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fermatNumber_zero proved · kernel-lean · F:ml430-nat-fermatnumber-zero-ca7aac67 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_add proved · kernel-lean · F:ml430-nat-fib-add-81ea2485 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_add_two proved · kernel-lean · F:ml430-nat-fib-add-two-b86e0c82 1 dependencies
11 dependents
-
Mathlib v4.30 source proposition Nat.fib_add_two_strictMono proved · kernel-lean · F:ml430-nat-fib-add-two-strictmono-c1e86d4d 13 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.fib_coprime_fib_succ proved · kernel-lean · F:ml430-nat-fib-coprime-fib-succ-162fc738 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.fib_dvd proved · kernel-lean · F:ml430-nat-fib-dvd-f80f3de1 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_eq_zero proved · kernel-lean · F:ml430-nat-fib-eq-zero-61879073 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_gcd proved · kernel-lean · F:ml430-nat-fib-gcd-d1d98407 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.fib_le_fib_succ proved · kernel-lean · F:ml430-nat-fib-le-fib-succ-d1ef4a3d 4 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.fib_lt_fib proved · kernel-lean · F:ml430-nat-fib-lt-fib-3582b881 6 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.fib_lt_fib_succ proved · kernel-lean · F:ml430-nat-fib-lt-fib-succ-b4305b68 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_mono proved · kernel-lean · F:ml430-nat-fib-mono-cc6afe09 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.fib_one proved · kernel-lean · F:ml430-nat-fib-one-02785c52 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_pos proved · kernel-lean · F:ml430-nat-fib-pos-9e67bd8e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.fib_strictMonoOn proved · kernel-lean · F:ml430-nat-fib-strictmonoon-905810a9 7 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.fib_two proved · kernel-lean · F:ml430-nat-fib-two-2f3715f3 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_eq open · route not assigned · F:ml430-nat-findgreatest-eq-87c06f0f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_eq_iff open · route not assigned · F:ml430-nat-findgreatest-eq-iff-426770ce 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_eq_zero_iff open · route not assigned · F:ml430-nat-findgreatest-eq-zero-iff-3498d512 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_is_greatest open · route not assigned · F:ml430-nat-findgreatest-is-greatest-27ee7d92 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_le open · route not assigned · F:ml430-nat-findgreatest-le-8e41e6aa 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_mono open · route not assigned · F:ml430-nat-findgreatest-mono-2566201e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_mono_left open · route not assigned · F:ml430-nat-findgreatest-mono-left-065903af 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_mono_right open · route not assigned · F:ml430-nat-findgreatest-mono-right-8d67c0d3 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_of_ne_zero open · route not assigned · F:ml430-nat-findgreatest-of-ne-zero-04670c87 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.findGreatest_of_not open · route not assigned · F:ml430-nat-findgreatest-of-not-0229e05d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.floorRoot_eq_zero open · route not assigned · F:ml430-nat-floorroot-eq-zero-a3be4438 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.forall_ne_zero_iff open · route not assigned · F:ml430-nat-forall-ne-zero-iff-37819136 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.gcd_dvd_mul proved · kernel-lean · F:ml430-nat-gcd-dvd-mul-81cb13df 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.gcd_fib_add_self proved · kernel-lean · F:ml430-nat-gcd-fib-add-self-5a92d5e3 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.gcd_greatest proved · kernel-lean · F:ml430-nat-gcd-greatest-0a04214a 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.gcd_le_mul proved · kernel-lean · F:ml430-nat-gcd-le-mul-7e3800f7 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.gcd_mul_lcm proved · kernel-lean · F:ml430-nat-gcd-mul-lcm-b7217ace 9 dependencies
6 dependents
-
Mathlib v4.30 source proposition Nat.induct_rcc_left open · route not assigned · F:ml430-nat-induct-rcc-left-4c2df6c6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.induct_rcc_right open · route not assigned · F:ml430-nat-induct-rcc-right-daac46fe 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.land_assoc proved · kernel-lean · F:ml430-nat-land-assoc-ad4775b8 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.land_bit proved · kernel-lean · F:ml430-nat-land-bit-b9ab7475 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.land_comm proved · kernel-lean · F:ml430-nat-land-comm-7e6ad72e 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.lcm_assoc proved · kernel-lean · F:ml430-nat-lcm-assoc-cb00bb43 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lcm_comm proved · kernel-lean · F:ml430-nat-lcm-comm-d5f8aae0 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lcm_div proved · kernel-lean · F:ml430-nat-lcm-div-eb5d8892 18 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lcm_dvd proved · kernel-lean · F:ml430-nat-lcm-dvd-07899eea 12 dependencies
6 dependents
-
Mathlib v4.30 source proposition Nat.lcmUpto_dvd_factorial open · route not assigned · F:ml430-nat-lcmupto-dvd-factorial-713c6bc6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lcmUpto_ne_zero open · route not assigned · F:ml430-nat-lcmupto-ne-zero-418388ac 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lcmUpto_pos open · route not assigned · F:ml430-nat-lcmupto-pos-e4917519 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ldiff_bit proved · kernel-lean · F:ml430-nat-ldiff-bit-6be49bb8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_add_one_of_avg_eq_left open · route not assigned · F:ml430-nat-le-add-one-of-avg-eq-left-210e3373 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_add_one_of_avg_eq_right open · route not assigned · F:ml430-nat-le-add-one-of-avg-eq-right-58e5e606 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_antisymm proved · kernel-lean · F:ml430-nat-le-antisymm-79dccead 2 dependencies
53 dependents
-
Mathlib v4.30 source proposition Nat.le_avg_left open · route not assigned · F:ml430-nat-le-avg-left-5067bf7f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_avg_right open · route not assigned · F:ml430-nat-le-avg-right-3a424d9e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_div_two_iff_mul_two_le open · route not assigned · F:ml430-nat-le-div-two-iff-mul-two-le-28da1d50 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_fib_add_one proved · kernel-lean · F:ml430-nat-le-fib-add-one-5284f0bf 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_fib_self proved · kernel-lean · F:ml430-nat-le-fib-self-0cbccb4d 11 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.le_induction open · route not assigned · F:ml430-nat-le-induction-2f088ac3 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_max_left proved · kernel-lean · F:ml430-nat-le-max-left-685a3331 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_max_right proved · kernel-lean · F:ml430-nat-le-max-right-3cd92fc9 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_min proved · kernel-lean · F:ml430-nat-le-min-69904590 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.le_min_of_le_of_le proved · kernel-lean · F:ml430-nat-le-min-of-le-of-le-407ecd4b 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.le_nth_of_lt_nth_succ open · route not assigned · F:ml430-nat-le-nth-of-lt-nth-succ-6d69133f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_nthRoot_iff open · route not assigned · F:ml430-nat-le-nthroot-iff-82e243be 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_of_ble_eq_true proved · kernel-lean · F:ml430-nat-le-of-ble-eq-true-646f4e10 2 dependencies
21 dependents
-
Mathlib v4.30 source proposition Nat.le_of_lt_succ proved · kernel-lean · F:ml430-nat-le-of-lt-succ-120bd6db 9 dependencies
51 dependents
-
Mathlib v4.30 source proposition Nat.le_of_succ_le_succ proved · kernel-lean · F:ml430-nat-le-of-succ-le-succ-a180a72c 1 dependencies
71 dependents
-
Mathlib v4.30 source proposition Nat.le_refl proved · kernel-lean · F:ml430-nat-le-refl-fd7d9e15 6 dependencies
16 dependents
-
Mathlib v4.30 source proposition Nat.le_sqrt open · route not assigned · F:ml430-nat-le-sqrt-e6996680 2 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.le_sqrt_of_eq_mul open · route not assigned · F:ml430-nat-le-sqrt-of-eq-mul-503c5afe 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_succ_iff_eq_or_le open · route not assigned · F:ml430-nat-le-succ-iff-eq-or-le-0cd6331b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_three_of_sqrt_eq_one open · route not assigned · F:ml430-nat-le-three-of-sqrt-eq-one-0c48a868 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.le_zero_eq open · route not assigned · F:ml430-nat-le-zero-eq-336b502d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_anti_left proved · kernel-lean · F:ml430-nat-log-anti-left-b72490ec 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_antitone_left proved · kernel-lean · F:ml430-nat-log-antitone-left-20d1326c 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.log_div_mul_self proved · kernel-lean · F:ml430-nat-log-div-mul-self-04282351 24 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_eq_one_iff' proved · kernel-lean · F:ml430-nat-log-eq-one-iff-63d772fb 20 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_eq_one_iff proved · kernel-lean · F:ml430-nat-log-eq-one-iff-a89f8bab 16 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_eq_zero_iff proved · kernel-lean · F:ml430-nat-log-eq-zero-iff-819cea74 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_le_clog proved · kernel-lean · F:ml430-nat-log-le-clog-ac8ab2d4 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_le_self proved · kernel-lean · F:ml430-nat-log-le-self-da387172 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_lt_self proved · kernel-lean · F:ml430-nat-log-lt-self-529f89fa 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.log_mono_right proved · kernel-lean · F:ml430-nat-log-mono-right-b8939fee 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.log_monotone proved · kernel-lean · F:ml430-nat-log-monotone-52fad774 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_of_lt proved · kernel-lean · F:ml430-nat-log-of-lt-89eaf42e 1 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.log_one_left proved · kernel-lean · F:ml430-nat-log-one-left-73efc119 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_one_right proved · kernel-lean · F:ml430-nat-log-one-right-282332ef 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_zero_left proved · kernel-lean · F:ml430-nat-log-zero-left-9ec8541e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.log_zero_right proved · kernel-lean · F:ml430-nat-log-zero-right-8ea186db 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.log2_eq_log_two proved · kernel-lean · F:ml430-nat-log2-eq-log-two-28085932 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lor_assoc proved · kernel-lean · F:ml430-nat-lor-assoc-82c4d0fd 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lor_bit proved · kernel-lean · F:ml430-nat-lor-bit-a2f98c7c 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.lor_comm proved · kernel-lean · F:ml430-nat-lor-comm-2666d7ef 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lt_min proved · kernel-lean · F:ml430-nat-lt-min-1a793099 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lt_of_mul_lt_mul_left proved · kernel-lean · F:ml430-nat-lt-of-mul-lt-mul-left-234e8530 4 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.lt_of_mul_lt_mul_right proved · kernel-lean · F:ml430-nat-lt-of-mul-lt-mul-right-54c1120b 5 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.lt_of_testBit open · route not assigned · F:ml430-nat-lt-of-testbit-72f64ab8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lt_pow_nthRoot_add_one open · route not assigned · F:ml430-nat-lt-pow-nthroot-add-one-7442ac90 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.lt_succ_sqrt open · route not assigned · F:ml430-nat-lt-succ-sqrt-39389df2 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.lt_xor_cases proved · kernel-lean · F:ml430-nat-lt-xor-cases-c43a1e85 10 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.max_comm proved · kernel-lean · F:ml430-nat-max-comm-a9a3642b 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mod_lcm proved · kernel-lean · F:ml430-nat-mod-lcm-ee6bdd41 C:least-common-multipleC:modular-arithmetic 14 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mod_modEq proved · kernel-lean · F:ml430-nat-mod-modeq-436e4c10 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mod_mul proved · kernel-lean · F:ml430-nat-mod-mul-beaccbad 20 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.mod_mul_left_div_self proved · kernel-lean · F:ml430-nat-mod-mul-left-div-self-0aca6c6e 25 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mod_mul_left_mod proved · kernel-lean · F:ml430-nat-mod-mul-left-mod-9b785abc 13 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mod_mul_right_div_self proved · kernel-lean · F:ml430-nat-mod-mul-right-div-self-900e0b01 24 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.mod_mul_right_mod proved · kernel-lean · F:ml430-nat-mod-mul-right-mod-a481eff8 12 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add proved · kernel-lean · F:ml430-nat-modeq-add-1561afa8 3 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_iff_left proved · kernel-lean · F:ml430-nat-modeq-add-iff-left-b719aac5 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_iff_right proved · kernel-lean · F:ml430-nat-modeq-add-iff-right-84daa45f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_le_of_lt proved · kernel-lean · F:ml430-nat-modeq-add-le-of-lt-c774015b 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_left_cancel' proved · kernel-lean · F:ml430-nat-modeq-add-left-cancel-e5287cf6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_left_cancel proved · kernel-lean · F:ml430-nat-modeq-add-left-cancel-fb96581c 6 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_left proved · kernel-lean · F:ml430-nat-modeq-add-left-e83f0700 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_right proved · kernel-lean · F:ml430-nat-modeq-add-right-8e2ca0cc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_right_cancel' proved · kernel-lean · F:ml430-nat-modeq-add-right-cancel-e871facf 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.add_right_cancel proved · kernel-lean · F:ml430-nat-modeq-add-right-cancel-f0ab48e4 6 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.cancel_left_div_gcd proved · kernel-lean · F:ml430-nat-modeq-cancel-left-div-gcd-57ef8287 9 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.cancel_left_div_gcd' proved · kernel-lean · F:ml430-nat-modeq-cancel-left-div-gcd-cfca1225 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.cancel_left_of_coprime proved · kernel-lean · F:ml430-nat-modeq-cancel-left-of-coprime-f89af373 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.cancel_right_div_gcd proved · kernel-lean · F:ml430-nat-modeq-cancel-right-div-gcd-22a4f40d 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.comm proved · kernel-lean · F:ml430-nat-modeq-comm-24b71e7a 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.dvd_iff proved · kernel-lean · F:ml430-nat-modeq-dvd-iff-8f130450 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.gcd_eq proved · kernel-lean · F:ml430-nat-modeq-gcd-eq-5167ff4f 14 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.of_dvd proved · kernel-lean · F:ml430-nat-modeq-of-dvd-d75cc374 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.of_mul_left proved · kernel-lean · F:ml430-nat-modeq-of-mul-left-88d20bca 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.of_mul_right proved · kernel-lean · F:ml430-nat-modeq-of-mul-right-43078e1c 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.modEq_one proved · kernel-lean · F:ml430-nat-modeq-one-516d46e8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.refl proved · kernel-lean · F:ml430-nat-modeq-refl-d870c8f5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.symm proved · kernel-lean · F:ml430-nat-modeq-symm-0a3d4d18 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.ModEq.trans proved · kernel-lean · F:ml430-nat-modeq-trans-ef9d1c46 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.modulus_modEq_zero proved · kernel-lean · F:ml430-nat-modulus-modeq-zero-fd9af096 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.monotone_primeCounting open · route not assigned · F:ml430-nat-monotone-primecounting-8c35da98 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.monotone_primeCounting' open · route not assigned · F:ml430-nat-monotone-primecounting-9ecb2222 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mul_add_lt_mul_of_lt_of_lt open · route not assigned · F:ml430-nat-mul-add-lt-mul-of-lt-of-lt-3567e87f 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.mul_lt_mul_left proved · kernel-lean · F:ml430-nat-mul-lt-mul-left-af33301e 4 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.mul_lt_mul_right proved · kernel-lean · F:ml430-nat-mul-lt-mul-right-de5b6046 6 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.multichoose_one open · route not assigned · F:ml430-nat-multichoose-one-b210386a 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.multichoose_one_right open · route not assigned · F:ml430-nat-multichoose-one-right-7755072d 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.multichoose_zero_right open · route not assigned · F:ml430-nat-multichoose-zero-right-6ef827c8 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.nat_repr_len_aux open · route not assigned · F:ml430-nat-nat-repr-len-aux-e53093d1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.not_coprime_zero_zero proved · kernel-lean · F:ml430-nat-not-coprime-zero-zero-6c4e8dd8 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.not_exists_sq open · route not assigned · F:ml430-nat-not-exists-sq-3678b0c0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.not_prime_of_dvd_of_ne proved · kernel-lean · F:ml430-nat-not-prime-of-dvd-of-ne-4ff592c0 0 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.not_two_dvd_bit1 open · route not assigned · F:ml430-nat-not-two-dvd-bit1-d5b4bf00 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_add open · route not assigned · F:ml430-nat-nth-add-a9dfaba9 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_add_one open · route not assigned · F:ml430-nat-nth-add-one-3fc46c88 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_eq_zero_mono open · route not assigned · F:ml430-nat-nth-eq-zero-mono-2dbbfdd5 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_false open · route not assigned · F:ml430-nat-nth-false-969b255e 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_mem_anti open · route not assigned · F:ml430-nat-nth-mem-anti-db30d674 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_mem_of_ne_zero open · route not assigned · F:ml430-nat-nth-mem-of-ne-zero-c1d86fab 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_ne_zero_anti open · route not assigned · F:ml430-nat-nth-ne-zero-anti-aab2a2dc 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_of_forall open · route not assigned · F:ml430-nat-nth-of-forall-eef6b587 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nth_true open · route not assigned · F:ml430-nat-nth-true-8ba7e1e1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot_eq_of_le_of_lt open · route not assigned · F:ml430-nat-nthroot-eq-of-le-of-lt-55ab78a4 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot_lt_iff open · route not assigned · F:ml430-nat-nthroot-lt-iff-a71b6995 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot.lt_pow_go_succ_aux open · route not assigned · F:ml430-nat-nthroot-lt-pow-go-succ-aux-7ebd25d8 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot_one_right open · route not assigned · F:ml430-nat-nthroot-one-right-9744d156 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot_pow open · route not assigned · F:ml430-nat-nthroot-pow-02612a4b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.nthRoot_zero_left open · route not assigned · F:ml430-nat-nthroot-zero-left-8560aafb 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.odd_fermatNumber proved · kernel-lean · F:ml430-nat-odd-fermatnumber-251041a5 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Odd.of_mul_left proved · kernel-lean · F:ml430-nat-odd-of-mul-left-2c6c2553 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Odd.of_mul_right proved · kernel-lean · F:ml430-nat-odd-of-mul-right-fe6d20ff 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.odd_totient_iff proved · kernel-lean · F:ml430-nat-odd-totient-iff-b6a6596f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.odd_totient_iff_eq_one proved · kernel-lean · F:ml430-nat-odd-totient-iff-eq-one-d0491d84 9 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.one_ascFactorial proved · kernel-lean · F:ml430-nat-one-ascfactorial-8bacb017 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.pow_of_pow_add_prime proved · kernel-lean · F:ml430-nat-pow-of-pow-add-prime-ab61d0d3 13 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.coprime_choose_of_lt open · route not assigned · F:ml430-nat-prime-coprime-choose-of-lt-3ccff0b4 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.coprime_descFactorial_of_lt_of_le proved · kernel-lean · F:ml430-nat-prime-coprime-descfactorial-of-lt-of-le-716dffc3 14 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.coprime_factorial_of_lt proved · kernel-lean · F:ml430-nat-prime-coprime-factorial-of-lt-2dbea201 9 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Prime.coprime_iff_not_dvd proved · kernel-lean · F:ml430-nat-prime-coprime-iff-not-dvd-a85d46a4 5 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.coprime_pow_of_not_dvd proved · kernel-lean · F:ml430-nat-prime-coprime-pow-of-not-dvd-2752b17f 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.deficient proved · kernel-lean · F:ml430-nat-prime-deficient-89e0badf 5 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Prime.deficient_pow open · route not assigned · F:ml430-nat-prime-deficient-pow-9c5e1fef 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_choose_add open · route not assigned · F:ml430-nat-prime-dvd-choose-add-235cc461 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_choose_self open · route not assigned · F:ml430-nat-prime-dvd-choose-self-b81c2438 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_factorial proved · kernel-lean · F:ml430-nat-prime-dvd-factorial-5ace903f 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_iff_eq proved · kernel-lean · F:ml430-nat-prime-dvd-iff-eq-b7446896 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_iff_not_coprime proved · kernel-lean · F:ml430-nat-prime-dvd-iff-not-coprime-77854741 C:prime-numberC:greatest-common-divisor 12 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_lcm proved · kernel-lean · F:ml430-nat-prime-dvd-lcm-237d267c 10 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_mul proved · kernel-lean · F:ml430-nat-prime-dvd-mul-59446847 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_mul_of_dvd_ne proved · kernel-lean · F:ml430-nat-prime-dvd-mul-of-dvd-ne-6c253439 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_of_dvd_pow proved · kernel-lean · F:ml430-nat-prime-dvd-of-dvd-pow-e76f834a 10 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_or_dvd proved · kernel-lean · F:ml430-nat-prime-dvd-or-dvd-4ae88221 15 dependencies
8 dependents
-
Mathlib v4.30 source proposition Nat.Prime.dvd_or_dvd_of_dvd_lcm proved · kernel-lean · F:ml430-nat-prime-dvd-or-dvd-of-dvd-lcm-58280948 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.eq_one_of_pow proved · kernel-lean · F:ml430-nat-prime-eq-one-of-pow-846d2949 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.eq_one_or_self_of_dvd proved · kernel-lean · F:ml430-nat-prime-eq-one-or-self-of-dvd-48de0abb 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.eq_two_or_odd' proved · kernel-lean · F:ml430-nat-prime-eq-two-or-odd-25691fc9 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.eq_two_or_odd proved · kernel-lean · F:ml430-nat-prime-eq-two-or-odd-44a91651 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.even_iff proved · kernel-lean · F:ml430-nat-prime-even-iff-d068ec82 15 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.Prime.five_le_of_ne_two_of_ne_three proved · kernel-lean · F:ml430-nat-prime-five-le-of-ne-two-of-ne-three-c069e786 15 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.mod_two_eq_one_iff_ne_two proved · kernel-lean · F:ml430-nat-prime-mod-two-eq-one-iff-ne-two-25c35e73 3 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.mul_eq_prime_sq_iff proved · kernel-lean · F:ml430-nat-prime-mul-eq-prime-sq-iff-d3fd2e31 11 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.ne_one proved · kernel-lean · F:ml430-nat-prime-ne-one-5b7f8845 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.ne_zero proved · kernel-lean · F:ml430-nat-prime-ne-zero-b4e8b4d5 3 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_abundant proved · kernel-lean · F:ml430-nat-prime-not-abundant-d2558ed6 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_coprime_iff_dvd proved · kernel-lean · F:ml430-nat-prime-not-coprime-iff-dvd-c83110ca 16 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_dvd_mul proved · kernel-lean · F:ml430-nat-prime-not-dvd-mul-cb3a915e 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_dvd_one proved · kernel-lean · F:ml430-nat-prime-not-dvd-one-be7e780f 1 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_perfect proved · kernel-lean · F:ml430-nat-prime-not-perfect-15c1235d 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_prime_pow' proved · kernel-lean · F:ml430-nat-prime-not-prime-pow-5f14afc6 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.not_prime_pow proved · kernel-lean · F:ml430-nat-prime-not-prime-pow-d6480abf 9 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.odd_of_ne_two proved · kernel-lean · F:ml430-nat-prime-odd-of-ne-two-91e1195f 12 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.one_le proved · kernel-lean · F:ml430-nat-prime-one-le-03eb3095 2 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.Prime.one_lt proved · kernel-lean · F:ml430-nat-prime-one-lt-bc90cfc7 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.Prime.pos proved · kernel-lean · F:ml430-nat-prime-pos-85eeeeea 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.pred_pos proved · kernel-lean · F:ml430-nat-prime-pred-pos-4e67ac4c 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Prime.sum_four_squares open · route not assigned · F:ml430-nat-prime-sum-four-squares-a60fd297 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.primeCounting'_add_le open · route not assigned · F:ml430-nat-primecounting-add-le-1ce4f43d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.primeCounting_add_le open · route not assigned · F:ml430-nat-primecounting-add-le-3fef2bb6 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.primeCounting'_eq_zero_iff open · route not assigned · F:ml430-nat-primecounting-eq-zero-iff-b4a33465 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.add open · route not assigned · F:ml430-nat-primrec-add-ea539e24 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.casesOn' open · route not assigned · F:ml430-nat-primrec-caseson-68977e97 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.casesOn1 open · route not assigned · F:ml430-nat-primrec-caseson1-f533b9fe 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.const open · route not assigned · F:ml430-nat-primrec-const-a120c9a1 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.mul open · route not assigned · F:ml430-nat-primrec-mul-2e55be0c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.of_eq open · route not assigned · F:ml430-nat-primrec-of-eq-d42f5250 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.pow open · route not assigned · F:ml430-nat-primrec-pow-cf3df8b0 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.prec1 open · route not assigned · F:ml430-nat-primrec-prec1-61e68b20 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.pred open · route not assigned · F:ml430-nat-primrec-pred-57bf43f2 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Primrec.swap open · route not assigned · F:ml430-nat-primrec-swap-eab7e860 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.self_le_factorial proved · kernel-lean · F:ml430-nat-self-le-factorial-cfdffc69 7 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Simproc.le_add_le open · route not assigned · F:ml430-nat-simproc-le-add-le-bc6f7c5c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.size_bit proved · kernel-lean · F:ml430-nat-size-bit-c601dbf0 13 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.size_eq_zero proved · kernel-lean · F:ml430-nat-size-eq-zero-020ad98c 5 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.size_le_size proved · kernel-lean · F:ml430-nat-size-le-size-c4b98f53 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.size_one proved · kernel-lean · F:ml430-nat-size-one-e23e5f71 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sq_add_sq_mul open · route not assigned · F:ml430-nat-sq-add-sq-mul-7964e174 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_eq open · route not assigned · F:ml430-nat-sqrt-eq-79ae8eae 0 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_eq' open · route not assigned · F:ml430-nat-sqrt-eq-c036815b 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_eq_zero open · route not assigned · F:ml430-nat-sqrt-eq-zero-53666a3b 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_le open · route not assigned · F:ml430-nat-sqrt-le-7918582b 0 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_le_self open · route not assigned · F:ml430-nat-sqrt-le-self-1ed5eb85 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_le_sqrt open · route not assigned · F:ml430-nat-sqrt-le-sqrt-6e2bfc47 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_lt open · route not assigned · F:ml430-nat-sqrt-lt-4909537f 0 dependencies
4 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_lt_self open · route not assigned · F:ml430-nat-sqrt-lt-self-ff7a155a 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_pos open · route not assigned · F:ml430-nat-sqrt-pos-f75e5114 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sqrt_succ_le_succ_sqrt open · route not assigned · F:ml430-nat-sqrt-succ-le-succ-sqrt-6b041183 1 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.Squarefree.ext_iff open · route not assigned · F:ml430-nat-squarefree-ext-iff-7218327d 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_eq_zero_of_lt proved · kernel-lean · F:ml430-nat-stirlingfirst-eq-zero-of-lt-6f46764f 4 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_one_right proved · kernel-lean · F:ml430-nat-stirlingfirst-one-right-84dfc371 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_self proved · kernel-lean · F:ml430-nat-stirlingfirst-self-4d06a0eb 2 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_succ_self_left proved · kernel-lean · F:ml430-nat-stirlingfirst-succ-self-left-135bbfbf 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_succ_succ proved · kernel-lean · F:ml430-nat-stirlingfirst-succ-succ-61c94738 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_succ_zero proved · kernel-lean · F:ml430-nat-stirlingfirst-succ-zero-a58c6f3c 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_zero proved · kernel-lean · F:ml430-nat-stirlingfirst-zero-ae5f4939 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingFirst_zero_succ proved · kernel-lean · F:ml430-nat-stirlingfirst-zero-succ-d25889f3 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingSecond_eq_zero_of_lt proved · kernel-lean · F:ml430-nat-stirlingsecond-eq-zero-of-lt-f3caf8bd 4 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.stirlingSecond_one_right proved · kernel-lean · F:ml430-nat-stirlingsecond-one-right-ef2ad447 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.succ_pred_prime proved · kernel-lean · F:ml430-nat-succ-pred-prime-4feb123f 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.sum_four_squares open · route not assigned · F:ml430-nat-sum-four-squares-5cfacf06 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.testBit_eq_inth open · route not assigned · F:ml430-nat-testbit-eq-inth-ffa07392 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.testBit_land open · route not assigned · F:ml430-nat-testbit-land-dfef7ca4 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.testBit_ldiff open · route not assigned · F:ml430-nat-testbit-ldiff-16f94162 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.testBit_lor open · route not assigned · F:ml430-nat-testbit-lor-7644e067 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.totient_coprime_totient_iff proved · kernel-lean · F:ml430-nat-totient-coprime-totient-iff-3932cf83 18 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.totient_dvd_of_dvd proved · kernel-lean · F:ml430-nat-totient-dvd-of-dvd-9622e44a C:eulers-totient-functionC:divisibility 1 dependencies
1 dependents
-
Mathlib v4.30 source proposition Nat.totient_eq_one_iff proved · kernel-lean · F:ml430-nat-totient-eq-one-iff-68d883a0 16 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.totient_eq_zero proved · kernel-lean · F:ml430-nat-totient-eq-zero-3be161d6 2 dependencies
3 dependents
-
Mathlib v4.30 source proposition Nat.totient_even proved · kernel-lean · F:ml430-nat-totient-even-28e0415f 31 dependencies
2 dependents
-
Mathlib v4.30 source proposition Nat.totient_gcd_mul_totient_mul proved · kernel-lean · F:ml430-nat-totient-gcd-mul-totient-mul-2e1d13c7 C:eulers-totient-functionC:divisibility 2 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.zero_ascFactorial proved · kernel-lean · F:ml430-nat-zero-ascfactorial-af4fcdca 0 dependencies
0 dependents
-
Mathlib v4.30 source proposition Nat.zero_of_testBit_eq_false open · route not assigned · F:ml430-nat-zero-of-testbit-eq-false-e244c9a1 0 dependencies
0 dependents
-
Modus ponens is a valid inference proved · smt-term-level · F:modus-ponens-valid C:modus-ponensC:inference-ruleC:valid-argument 0 dependencies
1 dependents
-
Modus tollens is a valid inference proved · smt-term-level · F:modus-tollens-valid C:modus-tollensC:inference-ruleC:contrapositive 2 dependencies
0 dependents
-
NAND defines negation, conjunction and disjunction proved · smt-term-level · F:nand-functional-completeness C:nandC:logical-connectiveC:logical-equivalence 0 dependencies
0 dependents
-
Addition on the naturals is associative proved · kernel-lean · F:nat-add-assoc C:associativityC:addition 0 dependencies
58 dependents
-
Addition on the naturals is commutative proved · kernel-lean · F:nat-add-comm C:commutativity 2 dependencies
114 dependents
-
0 dependencies
36 dependents
-
3 dependencies
32 dependents
-
3 dependencies
10 dependents
-
1 dependencies
22 dependents
-
22 dependencies
2 dependents
-
4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
23 dependencies
2 dependents
-
Addition cancels on the right proved · kernel-lean · F:nat-add-right-cancel C:additionC:inverse-operation 1 dependencies
9 dependents
-
4 dependencies
26 dependents
-
Subtraction undoes addition on the naturals proved · kernel-lean · F:nat-add-sub-cancel-left C:inverse-operationC:subtractionC:addition 5 dependencies
13 dependents
-
3 dependencies
5 dependents
-
0 dependencies
16 dependents
-
Zero is a right identity for addition on the naturals proved · kernel-lean · F:nat-add-zero C:identity-elementC:zeroC:addition 0 dependencies
43 dependents
-
ascFactorial(n, 1) = n proved · kernel-lean · F:nat-asc-factorial-one 3 dependencies
0 dependents
-
1 dependencies
1 dependents
-
ascFactorial(n, 0) = 1 proved · kernel-lean · F:nat-asc-factorial-zero 0 dependencies
3 dependents
-
2 dependencies
15 dependents
-
3 dependencies
0 dependents
-
1 dependencies
18 dependents
-
0 dependencies
1 dependents
-
4 dependencies
1 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
9 dependencies
1 dependents
-
6 dependencies
1 dependents
-
1 dependencies
0 dependents
-
bit(false, n) <= bit(true, n) proved · kernel-lean · F:nat-bit-false-le-bit-true 2 dependencies
0 dependents
-
bit(false, n) = 2n proved · kernel-lean · F:nat-bit-false 0 dependencies
1 dependents
-
0 < bit(true, n) proved · kernel-lean · F:nat-bit-true-pos 3 dependencies
0 dependents
-
bit(true, n) = 2n + 1 proved · kernel-lean · F:nat-bit-true 0 dependencies
2 dependents
-
bitwise and_fn 3 5 = land 3 5 proved · kernel-lean · F:nat-bitwise-and-eq-land-three-five 0 dependencies
1 dependents
-
bitwise and_fn m n = land m n, for all m and n proved · kernel-lean · F:nat-bitwise-and-eq-land 2 dependencies
0 dependents
-
4 dependencies
0 dependents
-
bitwise is commutative for a commutative combinator proved · kernel-lean · F:nat-bitwise-comm C:bitwise-operations 3 dependencies
0 dependents
-
bitwise or_fn 3 5 = lor 3 5 proved · kernel-lean · F:nat-bitwise-or-eq-lor-three-five 0 dependencies
1 dependents
-
bitwise or_fn m n = lor m n, for all m and n proved · kernel-lean · F:nat-bitwise-or-eq-lor 2 dependencies
0 dependents
-
bitwise commutes with swapping the combinator's argument order proved · kernel-lean · F:nat-bitwise-swap C:bitwise-operations 3 dependencies
0 dependents
-
bitwise xor_fn 3 5 = 6 proved · kernel-lean · F:nat-bitwise-xor-three-five 0 dependencies
0 dependents
-
bitwise f 0 n = if f false true then n else 0 proved · kernel-lean · F:nat-bitwise-zero-left 0 dependencies
0 dependents
-
bitwise f m 0 = if f true false then m else 0 proved · kernel-lean · F:nat-bitwise-zero-right 0 dependencies
1 dependents
-
The boolean order test is false above its bound proved · kernel-lean · F:nat-ble-eq-false-of-lt 4 dependencies
8 dependents
-
4 dependencies
11 dependents
-
6 dependencies
1 dependents
-
0 dependencies
1 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
2 dependencies
1 dependents
-
0 dependencies
0 dependents
-
9 dependencies
0 dependents
-
20 dependencies
1 dependents
-
A binomial coefficient is bounded by the corresponding power of two proved · kernel-lean · F:nat-choose-le-two-pow C:binomial-coefficientC:counting 3 dependencies
0 dependents
-
C(a, a) = 1 proved · kernel-lean · F:nat-choose-self C:binomial-coefficient 2 dependencies
5 dependents
-
A binomial coefficient above the diagonal is zero proved · kernel-lean · F:nat-choose-succ-self-eq-zero C:binomial-coefficient 2 dependencies
3 dependents
-
Pascal's rule for binomial coefficients proved · kernel-lean · F:nat-choose-succ-succ C:binomial-coefficient 0 dependencies
10 dependents
-
Binomial coefficients are symmetric proved · kernel-lean · F:nat-choose-symm C:binomial-coefficientC:counting 17 dependencies
3 dependents
-
Choosing zero elements has exactly one way proved · kernel-lean · F:nat-choose-zero-right C:binomial-coefficientC:counting 0 dependencies
9 dependents
-
The ceiling logarithm in base one is zero proved · kernel-lean · F:nat-clog-one-left 0 dependencies
0 dependents
-
The ceiling logarithm at n = 1 is zero proved · kernel-lean · F:nat-clog-one-right 0 dependencies
0 dependents
-
The ceiling logarithm in base zero is zero proved · kernel-lean · F:nat-clog-zero-left 0 dependencies
0 dependents
-
The ceiling logarithm at n = 0 is zero proved · kernel-lean · F:nat-clog-zero-right 0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
2 dependents
-
0 dependencies
2 dependents
-
10 dependencies
0 dependents
-
3 dependencies
1 dependents
-
4 dependencies
2 dependents
-
A Bezout witness of 1 certifies coprimality proved · kernel-lean · F:nat-coprime-of-bezout-one C:greatest-common-divisorC:coprimeC:bezout-identity 17 dependencies
1 dependents
-
a number below minFac(n) and not zero is coprime to n proved · kernel-lean · F:nat-coprime-of-lt-minfac C:coprime-numbers 16 dependencies
0 dependents
-
5 dependencies
4 dependents
-
1 dependencies
0 dependents
-
15 dependencies
2 dependents
-
3 dependencies
1 dependents
-
0 dependencies
5 dependents
-
3 dependencies
1 dependents
-
0 dependencies
2 dependents
-
4 dependencies
2 dependents
-
4 dependencies
1 dependents
-
4 dependencies
2 dependents
-
The floor-counting lemma in executable form proved · kernel-lean · F:nat-countrange-mul-succ-le-eq-floor 2 dependencies
1 dependents
-
8 dependencies
1 dependents
-
3 dependencies
2 dependents
-
7 dependencies
1 dependents
-
0 dependencies
3 dependents
-
4 dependencies
1 dependents
-
0 dependencies
4 dependents
-
1 dependencies
0 dependents
-
7 dependencies
2 dependents
-
The CRT residue-pairing self-map is injective on a block of coprime dimensions proved · kernel-lean · F:nat-crt-self-map-injective-on C:chinese-remainder-theoremC:eulers-totient-function 8 dependencies
1 dependents
-
13 dependencies
2 dependents
-
n < k implies descFactorial(n, k) = 0 proved · kernel-lean · F:nat-desc-factorial-of-lt 8 dependencies
0 dependents
-
descFactorial(n, 1) = n proved · kernel-lean · F:nat-desc-factorial-one 3 dependencies
0 dependents
-
1 dependencies
3 dependents
-
descFactorial(n, 0) = 1 proved · kernel-lean · F:nat-desc-factorial-zero 0 dependencies
2 dependents
-
2 dependencies
9 dependents
-
2 dependencies
6 dependents
-
1 dependencies
1 dependents
-
The computed quotient and remainder satisfy the division specification proved · kernel-lean · F:nat-div-mod-exec C:division-algorithmC:divisionC:remainder 8 dependencies
54 dependents
-
Division with remainder always exists for a positive divisor proved · kernel-lean · F:nat-div-mod-exists C:division-algorithmC:divisionC:remainder 1 dependencies
5 dependents
-
7 dependencies
11 dependents
-
7 dependencies
2 dependents
-
2 dependencies
2 dependents
-
4 dependencies
5 dependents
-
3 dependencies
1 dependents
-
The quotient and remainder of a division are unique proved · kernel-lean · F:nat-div-mod-unique C:division-algorithmC:remainder 9 dependencies
28 dependents
-
5 dependencies
16 dependents
-
15 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
5 dependents
-
4 dependencies
4 dependents
-
Divisibility cancels out of a sum on the right proved · kernel-lean · F:nat-dvd-add-right-cancel-of-pos C:divisibilityC:addition 7 dependencies
8 dependents
-
A common divisor of two numbers divides their sum proved · kernel-lean · F:nat-dvd-add C:divisibilityC:factorC:multiple 1 dependencies
11 dependents
-
6 dependencies
8 dependents
-
A positive natural up to n divides n! proved · kernel-lean · F:nat-dvd-factorial-of-le C:factorialC:divisibility 9 dependencies
2 dependents
-
The gcd is exactly the common divisors' upper bound proved · kernel-lean · F:nat-dvd-gcd-iff C:greatest-common-divisorC:divisibilityC:coprime 5 dependencies
1 dependents
-
A common divisor divides the gcd proved · kernel-lean · F:nat-dvd-gcd C:greatest-common-divisorC:divisibility 6 dependencies
16 dependents
-
13 dependencies
6 dependents
-
12 dependencies
6 dependents
-
A divisor of the modulus decides divisibility of a value from its remainder proved · kernel-lean · F:nat-dvd-mod-iff C:divisibilityC:remainderC:modular-arithmetic 4 dependencies
4 dependents
-
Divisibility survives multiplying the dividend proved · kernel-lean · F:nat-dvd-mul-right-of-dvd C:divisibilityC:multiplication 3 dependencies
18 dependents
-
A factor divides its product proved · kernel-lean · F:nat-dvd-mul C:divisibilityC:factorC:multiplication 0 dependencies
28 dependents
-
6 dependencies
1 dependents
-
7 dependencies
1 dependents
-
Divisibility is reflexive proved · kernel-lean · F:nat-dvd-refl C:divisibility 1 dependencies
19 dependents
-
4 dependencies
1 dependents
-
Divisibility is transitive proved · kernel-lean · F:nat-dvd-trans C:divisibilityC:transitivity 1 dependencies
24 dependents
-
15 dependencies
3 dependents
-
15 dependencies
0 dependents
-
10 dependencies
1 dependents
-
1 dependencies
11 dependents
-
Eisenstein's counting identity proved · kernel-lean · F:nat-eisenstein-count-identity 7 dependencies
1 dependents
-
Eisenstein's floor-sum identity without the min proved · kernel-lean · F:nat-eisenstein-floor-sum-min-free 7 dependencies
1 dependents
-
6 dependencies
1 dependents
-
Eisenstein's lemma as a congruence mod 2 proved · kernel-lean · F:nat-eisenstein-lemma-modeq 6 dependencies
0 dependents
-
12 dependencies
2 dependents
-
0 dependencies
0 dependents
-
0 dependencies
17 dependents
-
15 dependencies
5 dependents
-
Only 1 divides 1 proved · kernel-lean · F:nat-eq-one-of-dvd-one C:divisibility 5 dependencies
18 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Euclid's lemma: a prime dividing a product divides a factor proved · kernel-lean · F:nat-euclid-lemma C:fundamental-theorem-of-arithmeticC:prime-numberC:divisibility 20 dependencies
8 dependents
-
9 dependencies
1 dependents
-
16 dependencies
3 dependents
-
Even (xor m n) iff Even m iff Even n proved · kernel-lean · F:nat-even-xor C:bitwise-xor 12 dependencies
0 dependents
-
1 dependencies
1 dependents
-
Every natural number at least 2 has a prime divisor proved · kernel-lean · F:nat-exists-prime-dvd C:prime-numberC:divisibilityC:infinitude-of-primes 11 dependencies
5 dependents
-
19 dependencies
0 dependents
-
There is no largest prime proved · kernel-lean · F:nat-exists-prime-gt C:infinitude-of-primesC:prime-number 11 dependencies
1 dependents
-
An exact divisibility exponent is unique proved · kernel-lean · F:nat-exponent-unique-of-exact-dvd 5 dependencies
1 dependents
-
0 dependencies
8 dependents
-
0 dependencies
2 dependents
-
0 dependencies
0 dependents
-
2 dependencies
9 dependents
-
11 dependencies
0 dependents
-
3 dependencies
2 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
4 dependencies
2 dependents
-
4 dependencies
2 dependents
-
Cardinality is monotone under decided inclusion proved · kernel-lean · F:nat-finset-card-le-of-subset 5 dependencies
0 dependents
-
Euler's totient is a finite-set cardinality proved · kernel-lean · F:nat-finset-card-totatives 1 dependencies
0 dependents
-
Inclusion-exclusion for a computed finite set proved · kernel-lean · F:nat-finset-card-union-add-card-inter 5 dependencies
0 dependents
-
Sums agree when the decided membership does proved · kernel-lean · F:nat-finset-sum-congr-of-beq 5 dependencies
0 dependents
-
Summing over a finite set past its own bound changes nothing proved · kernel-lean · F:nat-finset-sum-eq-sum-range-if-add 5 dependencies
2 dependents
-
A sum over a disjoint union splits proved · kernel-lean · F:nat-finset-sum-union-disjoint 8 dependencies
0 dependents
-
The signed Gauss fold preserves the sum over [1, m] proved · kernel-lean · F:nat-gauss-fold-sumrange-eq 5 dependencies
1 dependents
-
18 dependencies
11 dependents
-
7 dependencies
2 dependents
-
7 dependencies
0 dependents
-
Bezout's identity holds for the natural gcd proved · kernel-lean · F:nat-gcd-bezout C:bezout-identityC:greatest-common-divisor 16 dependencies
7 dependents
-
3 dependencies
3 dependents
-
The natural gcd divides its first argument proved · kernel-lean · F:nat-gcd-dvd-left C:greatest-common-divisorC:divisibility 1 dependencies
44 dependents
-
The natural gcd divides its second argument proved · kernel-lean · F:nat-gcd-dvd-right C:greatest-common-divisorC:divisibility 1 dependencies
40 dependents
-
The gcd divides both of its arguments proved · kernel-lean · F:nat-gcd-dvd C:greatest-common-divisorC:divisibility 8 dependencies
2 dependents
-
gcd times lcm recovers the product proved · kernel-lean · F:nat-gcd-mul-lcm C:greatest-common-divisorC:least-common-multiple 9 dependencies
3 dependents
-
The Euclidean algorithm's descent step is correct proved · kernel-lean · F:nat-gcd-succ C:euclidean-algorithmC:greatest-common-divisorC:remainder 4 dependencies
4 dependents
-
gcd(0, a) = a proved · kernel-lean · F:nat-gcd-zero-left C:greatest-common-divisorC:zero 4 dependencies
13 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
4 dependencies
1 dependents
-
0 dependencies
2 dependents
-
19 dependencies
6 dependents
-
7 dependencies
1 dependents
-
2 dependencies
0 dependents
-
29 dependencies
1 dependents
-
27 dependencies
1 dependents
-
15 dependencies
1 dependents
-
27 dependencies
1 dependents
-
6 dependencies
1 dependents
-
26 dependencies
1 dependents
-
15 dependencies
2 dependents
-
land is associative proved · kernel-lean · F:nat-land-assoc C:bitwise-and 6 dependencies
0 dependents
-
0 dependencies
2 dependents
-
land decodes through a bit-appended argument proved · kernel-lean · F:nat-land-bit C:bitwise-and 7 dependencies
0 dependents
-
land is commutative proved · kernel-lean · F:nat-land-comm C:bitwise-and 3 dependencies
1 dependents
-
land(1, 1) = 1 proved · kernel-lean · F:nat-land-one-one 0 dependencies
0 dependents
-
land(3, 5) = 1 proved · kernel-lean · F:nat-land-three-five 0 dependencies
0 dependents
-
land(0, n) = 0 proved · kernel-lean · F:nat-land-zero-left 0 dependencies
4 dependents
-
land(m, 0) = 0 proved · kernel-lean · F:nat-land-zero-right 1 dependencies
3 dependents
-
8 dependencies
0 dependents
-
13 dependencies
5 dependents
-
2 dependencies
7 dependents
-
ldiff decodes through a bit-appended argument proved · kernel-lean · F:nat-ldiff-bit C:bitwise-and 5 dependencies
0 dependents
-
ldiff(5, 3) = 4 proved · kernel-lean · F:nat-ldiff-five-three 1 dependencies
0 dependents
-
ldiff(3, 5) = 2 proved · kernel-lean · F:nat-ldiff-three-five 0 dependencies
1 dependents
-
ldiff(0, n) = 0 proved · kernel-lean · F:nat-ldiff-zero-left 0 dependencies
1 dependents
-
ldiff(m, 0) = m proved · kernel-lean · F:nat-ldiff-zero-right 1 dependencies
1 dependents
-
n is <= n plus anything proved · kernel-lean · F:nat-le-add-right C:order-relation 0 dependencies
103 dependents
-
<= on the naturals is antisymmetric proved · kernel-lean · F:nat-le-antisymm C:order-relation 3 dependencies
31 dependents
-
<= destructs into an additive witness proved · kernel-lean · F:nat-le-dest C:order-relationC:addition 0 dependencies
27 dependents
-
1 dependencies
1 dependents
-
5 dependencies
5 dependents
-
3 dependencies
14 dependents
-
2 dependencies
11 dependents
-
A divisor of a positive natural does not exceed it proved · kernel-lean · F:nat-le-of-dvd C:divisibilityC:order-relation 3 dependencies
32 dependents
-
10 dependencies
0 dependents
-
10 dependencies
30 dependents
-
6 dependencies
1 dependents
-
4 dependencies
2 dependents
-
<= cancels a shared successor proved · kernel-lean · F:nat-le-of-succ-le-succ C:order-relation 1 dependencies
58 dependents
-
The order on the naturals is reflexive proved · imported-kernel-lean · F:nat-le-refl C:order-relationC:natural-numbers 0 dependencies
4 dependents
-
7 dependencies
7 dependents
-
<= is preserved by successor on both sides proved · kernel-lean · F:nat-le-succ-succ C:order-relation 0 dependencies
155 dependents
-
Every natural number is below its successor proved · imported-kernel-lean · F:nat-le-succ C:order-relationC:natural-numbers 0 dependencies
4 dependents
-
9 dependencies
1 dependents
-
<= on the naturals is total proved · kernel-lean · F:nat-le-total C:order-relation 2 dependencies
56 dependents
-
<= on the naturals is transitive proved · kernel-lean · F:nat-le-trans C:order-relationC:transitivity 0 dependencies
198 dependents
-
11 dependencies
1 dependents
-
The least residues reconcile with the folded ones proved · kernel-lean · F:nat-leastresidue-sumrange-reconcile 13 dependencies
1 dependents
-
Multiplication distributes over addition on the left proved · kernel-lean · F:nat-left-distrib C:distributivityC:multiplicationC:addition 2 dependencies
34 dependents
-
1 dependencies
2 dependents
-
3 dependencies
0 dependents
-
The floor logarithm of n never exceeds n proved · kernel-lean · F:nat-log-le-self 1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
The floor logarithm in base one is zero proved · kernel-lean · F:nat-log-one-left 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The floor logarithm in base zero is zero proved · kernel-lean · F:nat-log-zero-left 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
3 dependencies
2 dependents
-
lor is associative proved · kernel-lean · F:nat-lor-assoc C:bitwise-or 4 dependencies
0 dependents
-
lor decodes through a bit-appended argument proved · kernel-lean · F:nat-lor-bit C:bitwise-or 5 dependencies
0 dependents
-
lor is commutative proved · kernel-lean · F:nat-lor-comm C:bitwise-or 3 dependencies
1 dependents
-
lor(3, 5) = 7 proved · kernel-lean · F:nat-lor-three-five 0 dependencies
0 dependents
-
lor(0, n) = n proved · kernel-lean · F:nat-lor-zero-left 0 dependencies
2 dependents
-
lor(m, 0) = m proved · kernel-lean · F:nat-lor-zero-right 1 dependencies
2 dependents
-
6 dependencies
1 dependents
-
< on the naturals is irreflexive proved · kernel-lean · F:nat-lt-irrefl C:order-relation 3 dependencies
77 dependents
-
2 dependencies
3 dependents
-
2 dependencies
32 dependents
-
1 dependencies
91 dependents
-
3 dependencies
1 dependents
-
21 dependencies
1 dependents
-
<= splits into < or = proved · kernel-lean · F:nat-lt-or-eq-of-le C:order-relation 1 dependencies
88 dependents
-
3 dependencies
37 dependents
-
1 dependencies
2 dependents
-
8 dependencies
9 dependents
-
6 dependencies
47 dependents
-
6 dependencies
1 dependents
-
12 dependencies
0 dependents
-
6 dependencies
1 dependents
-
2 dependencies
7 dependents
-
Congruence mod m is preserved by adding on the right proved · kernel-lean · F:nat-mod-eq-add-right C:congruenceC:modular-arithmeticC:addition 3 dependencies
8 dependents
-
3 dependencies
0 dependents
-
15 dependencies
2 dependents
-
2 dependencies
3 dependents
-
3 dependencies
1 dependents
-
Congruence mod m is preserved by multiplying on the left proved · kernel-lean · F:nat-mod-eq-mul-left C:congruenceC:modular-arithmeticC:multiplication 3 dependencies
3 dependents
-
Congruence mod m is preserved by multiplying on the right proved · kernel-lean · F:nat-mod-eq-mul-right C:congruenceC:modular-arithmeticC:multiplication 2 dependencies
3 dependents
-
Congruences may be multiplied proved · kernel-lean · F:nat-mod-eq-mul C:congruenceC:modular-arithmeticC:clock-arithmetic 3 dependencies
1 dependents
-
Congruence mod m is reflexive proved · kernel-lean · F:nat-mod-eq-refl C:congruenceC:modular-arithmetic 0 dependencies
5 dependents
-
7 dependencies
7 dependents
-
0 dependencies
8 dependents
-
Congruence mod m is transitive proved · kernel-lean · F:nat-mod-eq-trans C:congruenceC:modular-arithmeticC:transitivity 5 dependencies
11 dependents
-
Congruence to zero characterizes divisibility proved · kernel-lean · F:nat-mod-eq-zero-iff-dvd C:divisibilityC:modular-arithmetic 7 dependencies
2 dependents
-
A divisor's dividend is congruent to zero modulo it proved · kernel-lean · F:nat-mod-eq-zero-of-dvd C:divisibilityC:congruenceC:modular-arithmetic 3 dependencies
2 dependents
-
The remainder is smaller than a positive modulus proved · kernel-lean · F:nat-mod-lt C:division-algorithmC:euclidean-division 2 dependencies
23 dependents
-
4 dependencies
0 dependents
-
0 dependencies
0 dependents
-
n mod 2 = 0 or n mod 2 = 1 proved · kernel-lean · F:nat-mod-two-eq-zero-or-one 3 dependencies
7 dependents
-
16 dependencies
1 dependents
-
0 dependencies
8 dependents
-
20 dependencies
0 dependents
-
Congruence modulo m is an equivalence relation proved · kernel-lean · F:nat-modeq-equivalence-on C:modular-arithmeticC:congruenceC:equivalence-relation 3 dependencies
0 dependents
-
2 dependencies
1 dependents
-
1 dependencies
2 dependents
-
Multiplication on the naturals is associative proved · kernel-lean · F:nat-mul-assoc C:associativityC:multiplication 1 dependencies
54 dependents
-
Multiplication on the naturals is commutative proved · kernel-lean · F:nat-mul-comm C:commutativityC:multiplication 2 dependencies
105 dependents
-
3 dependencies
8 dependents
-
Multiplication by a fixed left factor preserves <= proved · kernel-lean · F:nat-mul-le-mul-left C:order-relationC:multiplication 2 dependencies
39 dependents
-
3 dependencies
32 dependents
-
No lattice point sits on the line through a coprime pair proved · kernel-lean · F:nat-mul-ne-mul-of-coprime-of-lt 4 dependencies
1 dependents
-
One is a right identity for multiplication on the naturals proved · kernel-lean · F:nat-mul-one C:identity-elementC:multiplication 1 dependencies
88 dependents
-
5 dependencies
4 dependents
-
6 dependencies
2 dependents
-
6 dependencies
2 dependents
-
The 1-based side condition the rectangle partition consumes proved · kernel-lean · F:nat-mul-succ-ne-mul-succ-of-coprime 3 dependencies
1 dependents
-
0 dependencies
15 dependents
-
The division algorithm, summed over a range proved · kernel-lean · F:nat-mul-sumrange-div-add-leastresidue 4 dependencies
1 dependents
-
3 dependencies
0 dependents
-
1 dependencies
4 dependents
-
Every natural times zero is zero proved · kernel-lean · F:nat-mul-zero C:multiplicationC:zero 0 dependencies
34 dependents
-
multichoose(n, 1) = n proved · kernel-lean · F:nat-multichoose-one-right 1 dependencies
0 dependents
-
multichoose(1, k) = 1 proved · kernel-lean · F:nat-multichoose-one 3 dependencies
0 dependents
-
multichoose(n, 0) = 1 proved · kernel-lean · F:nat-multichoose-zero-right 1 dependencies
0 dependents
-
A multiset of primes carries exactly its recorded multiplicity proved · kernel-lean · F:nat-multiset-not-pow-succ-count-dvd-prod 10 dependencies
1 dependents
-
4 dependencies
1 dependents
-
Uniqueness of prime factorization, as multiplicity agreement proved · kernel-lean · F:nat-multiset-prime-factorization-unique 7 dependencies
0 dependents
-
6 dependencies
0 dependents
-
The product of a singleton multiset is its element proved · kernel-lean · F:nat-multiset-prod-singleton 5 dependencies
0 dependents
-
1 dependencies
13 dependents
-
18 dependencies
0 dependents
-
8 dependencies
0 dependents
-
No natural of size at least 2 divides 1 proved · kernel-lean · F:nat-not-dvd-one-of-two-le C:divisibility 8 dependencies
9 dependents
-
2 dependencies
1 dependents
-
No natural number is less than zero proved · kernel-lean · F:nat-not-lt-zero C:order-relationC:zero 1 dependencies
28 dependents
-
4 dependencies
0 dependents
-
1 dependencies
17 dependents
-
No successor is <= zero proved · kernel-lean · F:nat-not-succ-le-zero C:order-relation 0 dependencies
51 dependents
-
The factorial of a natural number is always at least 1 proved · kernel-lean · F:nat-one-le-factorial C:factorialC:counting 4 dependencies
15 dependents
-
4 dependencies
1 dependents
-
6 dependencies
54 dependents
-
A divisor of a positive natural is itself positive proved · kernel-lean · F:nat-one-le-of-dvd-pos C:divisibilityC:order-relation 1 dependencies
28 dependents
-
4 dependencies
2 dependents
-
1 is a left identity for multiplication proved · kernel-lean · F:nat-one-mul C:multiplicationC:identity-element 3 dependencies
70 dependents
-
1 dependencies
7 dependents
-
2 dependencies
0 dependents
-
The constructed Nat is THE natural numbers, up to unique isomorphism proved · kernel-lean · F:nat-peano-categoricity C:peano-axiomsC:natural-numbers 0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
1 dependents
-
0 dependencies
1 dependents
-
0 dependencies
4 dependents
-
14 dependencies
2 dependents
-
8 dependencies
2 dependents
-
3 dependencies
0 dependents
-
The first index law: powers add over a product proved · kernel-lean · F:nat-pow-add C:index-lawsC:exponentC:power 4 dependencies
7 dependents
-
A power divides a higher power of the same base proved · kernel-lean · F:nat-pow-dvd-pow-of-le 3 dependencies
1 dependents
-
18 dependencies
2 dependents
-
4 dependencies
2 dependents
-
7 dependencies
3 dependents
-
6 dependencies
3 dependents
-
3 dependencies
0 dependents
-
7 dependencies
13 dependents
-
Fermat's little theorem for the naturals proved · kernel-lean · F:nat-pow-prime-modeq-self C:prime-numberC:modular-arithmeticC:fermats-little-theorem 8 dependencies
2 dependents
-
18 dependencies
1 dependents
-
1 dependencies
2 dependents
-
2 dependencies
0 dependents
-
2 dependencies
0 dependents
-
0 dependencies
16 dependents
-
10 dependencies
0 dependents
-
0 dependencies
12 dependents
-
5 dependencies
1 dependents
-
2 dependencies
4 dependents
-
0 dependencies
5 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
A prime divides the interior binomial coefficients of its own row proved · kernel-lean · F:nat-prime-dvd-choose C:prime-numberC:binomial-coefficientC:divisibility 12 dependencies
1 dependents
-
A prime power passes through a factor the prime does not divide proved · kernel-lean · F:nat-prime-pow-dvd-of-dvd-mul-of-not-dvd 11 dependencies
1 dependents
-
1 dependencies
0 dependents
-
Extending a product past its support changes nothing proved · kernel-lean · F:nat-prod-range-add-of-one-above 2 dependencies
1 dependents
-
0 dependencies
1 dependents
-
A product of ones is one proved · kernel-lean · F:nat-prod-range-eq-one-of-below 1 dependencies
1 dependents
-
2 dependencies
1 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
11 dependencies
2 dependents
-
13 dependencies
2 dependents
-
21 dependencies
0 dependents
-
23 dependencies
0 dependents
-
Multiplication distributes over addition on the right proved · kernel-lean · F:nat-right-distrib C:distributivityC:multiplicationC:addition 2 dependencies
12 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
21 dependencies
1 dependents
-
0 dependencies
1 dependents
-
sqrt(1) = 1 proved · kernel-lean · F:nat-sqrt-one 0 dependencies
0 dependents
-
sqrt(0) = 0 proved · kernel-lean · F:nat-sqrt-zero 0 dependencies
0 dependents
-
Subtraction undoes addition when the order holds proved · kernel-lean · F:nat-sub-add-cancel C:subtractionC:additionC:inverse-operation 4 dependencies
39 dependents
-
1 dependencies
5 dependents
-
10 dependencies
1 dependents
-
2 dependencies
4 dependents
-
4 dependencies
4 dependents
-
Every natural minus itself is zero proved · kernel-lean · F:nat-sub-self C:subtractionC:zero 1 dependencies
11 dependents
-
2 dependencies
1 dependents
-
0 dependencies
2 dependents
-
0 dependencies
4 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Nat succ_add proved · kernel-lean · F:nat-succ-add 0 dependencies
56 dependents
-
0 dependencies
21 dependents
-
8 dependencies
19 dependents
-
15 dependencies
3 dependents
-
(a+1) * b = a*b + b proved · kernel-lean · F:nat-succ-mul C:multiplicationC:addition 1 dependencies
40 dependents
-
0 dependencies
23 dependents
-
1 dependencies
53 dependents
-
2 dependencies
4 dependents
-
1 dependencies
0 dependents
-
Subtraction is unaffected by adding one to both sides proved · kernel-lean · F:nat-succ-sub-succ C:subtraction 0 dependencies
10 dependents
-
4 dependencies
1 dependents
-
5 dependencies
0 dependents
-
6 dependencies
0 dependents
-
3 dependencies
1 dependents
-
16 dependencies
3 dependents
-
0 dependencies
0 dependents
-
18 dependencies
1 dependents
-
27 dependencies
1 dependents
-
2 dependencies
0 dependents
-
4 dependencies
10 dependents
-
2 dependencies
12 dependents
-
0 dependencies
11 dependents
-
0 dependencies
3 dependents
-
10 dependencies
2 dependents
-
12 dependencies
1 dependents
-
8 dependencies
1 dependents
-
6 dependencies
0 dependents
-
3 dependencies
5 dependents
-
3 dependencies
5 dependents
-
0 dependencies
5 dependents
-
4 dependencies
1 dependents
-
0 dependencies
2 dependents
-
4 dependencies
0 dependents
-
2 dependencies
2 dependents
-
The conditional sum's successor equation proved · kernel-lean · F:nat-sumrangeif-succ 0 dependencies
0 dependents
-
The empty conditional sum is zero proved · kernel-lean · F:nat-sumrangeif-zero 0 dependencies
0 dependents
-
5 dependencies
0 dependents
-
14 dependencies
1 dependents
-
26 dependencies
3 dependents
-
5 dependencies
5 dependents
-
21 dependencies
2 dependents
-
0 dependencies
2 dependents
-
21 dependencies
7 dependents
-
0 dependencies
0 dependents
-
The prime step: multiplying by a prime preserves totient divisibility proved · kernel-lean · F:nat-totient-dvd-totient-mul-prime C:eulers-totient-functionC:prime-number 4 dependencies
1 dependents
-
Euler's totient is multiplicative on coprime arguments proved · kernel-lean · F:nat-totient-mul-of-coprime C:eulers-totient-functionC:chinese-remainder-theoremC:multiplicative-function 16 dependencies
3 dependents
-
Multiplying a modulus by one of its own divisors scales the totient exactly proved · kernel-lean · F:nat-totient-mul-of-dvd C:eulers-totient-functionC:divisibility 6 dependencies
3 dependents
-
Euler's totient at a prime power proved · kernel-lean · F:nat-totient-prime-pow C:eulers-totient-functionC:prime-number 9 dependencies
0 dependents
-
9 dependencies
1 dependents
-
1 dependencies
2 dependents
-
12 dependencies
1 dependents
-
2 dependencies
2 dependents
-
2 dependencies
12 dependents
-
0 dependencies
0 dependents
-
11 dependencies
0 dependents
-
xor is associative proved · kernel-lean · F:nat-xor-assoc 2 dependencies
1 dependents
-
xor a b != 0 iff a != b proved · kernel-lean · F:nat-xor-ne-zero-iff 5 dependencies
1 dependents
-
xor a (xor a b) = b proved · kernel-lean · F:nat-xor-xor-cancel-left 4 dependencies
2 dependents
-
xor(xor(a, b), b) = a proved · kernel-lean · F:nat-xor-xor-cancel-right 1 dependencies
1 dependents
-
Nat zero_add proved · kernel-lean · F:nat-zero-add 0 dependencies
91 dependents
-
A positive choice from zero is zero proved · kernel-lean · F:nat-zero-choose-succ C:binomial-coefficient 0 dependencies
4 dependents
-
0 dependencies
8 dependents
-
Zero is a lower bound for every natural number proved · kernel-lean · F:nat-zero-le C:order-relation 0 dependencies
209 dependents
-
2 dependencies
13 dependents
-
9 dependencies
34 dependents
-
0 dependencies
6 dependents
-
0 dependencies
55 dependents
-
a natural number with every bit zero is zero proved · kernel-lean · F:nat-zero-of-testbit-eq-zero 3 dependencies
1 dependents
-
10 dependencies
22 dependents
-
No integer squares to minus one proved · smt-term-level · F:no-integer-square-is-minus-one 0 dependencies
0 dependents
-
No proposition is equivalent to its own negation proved · smt-term-level · F:no-self-negating-proposition C:liar-paradoxC:russells-paradoxC:self-reference +1 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
A reconstructed Farkas refutation holds in every ordered commutative ring, and rests on no axiom proved · kernel-lean · F:ordered-ring-farkas-refutation C:ordered-ringC:linear-programming-duality 0 dependencies
1 dependents
-
2 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
2 dependents
-
Peirce's law proved · smt-term-level · F:peirce-law C:implicationC:if-then-statementC:intuitionism +1 0 dependencies
0 dependents
-
20 dependencies
1 dependents
-
Excluded middle for propositions, as Lean proves it proved · imported-kernel-lean · F:prop-excluded-middle-classical C:excluded-middleC:intuitionism 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
Negation exchanges the two quantifiers proved · smt-term-level · F:quantifier-negation-duality C:quantified-negationC:universal-quantifierC:existential-quantifier +1 0 dependencies
0 dependents
-
The four-colour Rado number of 5(x-y) = 3z is 625 computed · search-certificate · F:rado-r4-a5-b3 C:rado-number 0 dependencies
0 dependents
-
The four-colour Rado number of 5(x-y) = 4z is 741 computed · search-certificate · F:rado-r4-a5-b4 C:rado-number 0 dependencies
0 dependents
-
5 dependencies
0 dependents
-
3 dependencies
0 dependents
-
19 dependencies
0 dependents
-
5 dependencies
1 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
5 dependencies
0 dependents
-
Addition on the rationals is associative proved · kernel-lean · F:rat-add-assoc C:associativity 10 dependencies
79 dependents
-
Addition on the rationals is commutative proved · kernel-lean · F:rat-add-comm C:commutativity 5 dependencies
80 dependents
-
3 dependencies
5 dependents
-
Addition preserves the rational order in both arguments proved · kernel-lean · F:rat-add-le-add C:order-relation 9 dependencies
102 dependents
-
10 dependencies
2 dependents
-
6 dependencies
1 dependents
-
Rational addition renormalises and negation is an additive inverse proved · kernel-lean · F:rat-add-neg-inverse C:rational-arithmetic 1 dependencies
1 dependents
-
Every rational has an additive inverse proved · kernel-lean · F:rat-add-neg C:additive-inverse 8 dependencies
33 dependents
-
2 dependencies
11 dependents
-
4 dependencies
2 dependents
-
Zero is a right identity for rational addition proved · kernel-lean · F:rat-add-zero C:identity-element 6 dependencies
85 dependents
-
11 dependencies
1 dependents
-
20 dependencies
0 dependents
-
11 dependencies
0 dependents
-
3 dependencies
4 dependents
-
2 dependencies
0 dependents
-
3 dependencies
0 dependents
-
3 dependencies
0 dependents
-
A two-sided bound survives rational addition proved · kernel-lean · F:rat-bounds-add C:triangle-inequality 2 dependencies
38 dependents
-
A two-sided bound survives rational multiplication proved · kernel-lean · F:rat-bounds-mul C:triangle-inequality 10 dependencies
14 dependents
-
Negating a two-sided bound keeps it a bound proved · kernel-lean · F:rat-bounds-neg C:triangle-inequality 2 dependencies
38 dependents
-
15 dependencies
1 dependents
-
Chebyshev's inequality over the constructed rationals proved · kernel-lean · F:rat-chebyshev-inequality C:chebyshev-inequality 3 dependencies
1 dependents
-
3 dependencies
1 dependents
-
1 dependencies
4 dependents
-
1 dependencies
2 dependents
-
4 dependencies
1 dependents
-
7 dependencies
1 dependents
-
4 dependencies
1 dependents
-
Covariance is symmetric proved · kernel-lean · F:rat-covariance-comm 2 dependencies
4 dependents
-
5 dependencies
1 dependents
-
19 dependencies
2 dependents
-
19 dependencies
2 dependents
-
Cauchy-Schwarz for covariance: cov(X,Y)^2 <= var(X)*var(Y) proved · kernel-lean · F:rat-covariance-sq-le-variance-mul C:cauchy-schwarz-inequality 8 dependencies
0 dependents
-
11 dependencies
2 dependents
-
3 dependencies
0 dependents
-
10 dependencies
0 dependents
-
10 dependencies
0 dependents
-
10 dependencies
0 dependents
-
0 dependencies
1 dependents
-
A rational's denominator is always positive proved · kernel-lean · F:rat-den-pos C:rational-numbers 0 dependencies
34 dependents
-
6 dependencies
2 dependents
-
7 dependencies
1 dependents
-
2 dependencies
4 dependents
-
4 dependencies
5 dependents
-
6 dependencies
0 dependents
-
0 dependencies
0 dependents
-
6 dependencies
1 dependents
-
14 dependencies
1 dependents
-
5 dependencies
0 dependents
-
2 dependencies
0 dependents
-
9 dependencies
1 dependents
-
19 dependencies
1 dependents
-
10 dependencies
1 dependents
-
3 dependencies
0 dependents
-
8 dependencies
0 dependents
-
The 2x2 identity matrix over ℚ has determinant 1 proved · kernel-lean · F:rat-det2-id C:determinant 4 dependencies
0 dependents
-
6 dependencies
0 dependents
-
3 dependencies
0 dependents
-
2 dependencies
1 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
5 dependencies
0 dependents
-
4 dependencies
3 dependents
-
3 dependencies
0 dependents
-
3 dependencies
1 dependents
-
Cauchy-Schwarz for the finite rational dot product proved · kernel-lean · F:rat-dotn-cauchy-schwarz C:cauchy-schwarz-inequality 28 dependencies
0 dependents
-
The rational dot product is symmetric proved · kernel-lean · F:rat-dotn-comm C:inner-product 2 dependencies
1 dependents
-
2 dependencies
1 dependents
-
3 dependencies
1 dependents
-
0 dependencies
1 dependents
-
3 dependencies
0 dependents
-
0 dependencies
1 dependents
-
Two zero rows in a row pass the echelon step test proved · kernel-lean · F:rat-echelon-step-ok-both-cols 3 dependencies
1 dependents
-
2 dependencies
3 dependents
-
10 dependencies
14 dependents
-
2 dependencies
0 dependents
-
A rational with numerator zero is zero proved · kernel-lean · F:rat-eq-zero-of-num-zero 3 dependencies
4 dependents
-
2 dependencies
1 dependents
-
3 dependencies
4 dependents
-
2 dependencies
2 dependents
-
5 dependencies
0 dependents
-
2 dependencies
1 dependents
-
2 dependencies
1 dependents
-
3 dependencies
5 dependents
-
8 dependencies
0 dependents
-
4 dependencies
1 dependents
-
2 dependencies
0 dependents
-
3 dependencies
1 dependents
-
3 dependencies
0 dependents
-
0 dependencies
1 dependents
-
7 dependencies
28 dependents
-
4 dependencies
1 dependents
-
6 dependencies
7 dependents
-
3 dependencies
18 dependents
-
5 dependencies
7 dependents
-
8 dependencies
12 dependents
-
0 dependencies
0 dependents
-
2 dependencies
5 dependents
-
0 dependencies
1 dependents
-
5 dependencies
1 dependents
-
2 dependencies
2 dependents
-
3 dependencies
7 dependents
-
1 dependencies
18 dependents
-
Zero times an integer is zero proved · kernel-lean · F:rat-int-zero-mul 2 dependencies
21 dependents
-
Rational inversion reverses order on positives proved · kernel-lean · F:rat-inv-le-of-pos-le 9 dependencies
1 dependents
-
The reciprocal of 1/(n+1) is n+1 proved · kernel-lean · F:rat-inv-natdivsucc 10 dependencies
4 dependents
-
8 dependencies
6 dependents
-
5 dependencies
0 dependents
-
6 dependencies
1 dependents
-
7 dependencies
1 dependents
-
7 dependencies
1 dependents
-
6 dependencies
1 dependents
-
4 dependencies
2 dependents
-
0 dependencies
3 dependents
-
3 dependencies
1 dependents
-
1 dependencies
2 dependents
-
Rational order is antisymmetric proved · kernel-lean · F:rat-le-antisymm 2 dependencies
11 dependents
-
2 dependencies
12 dependents
-
2 dependencies
11 dependents
-
1 dependencies
1 dependents
-
2 dependencies
0 dependents
-
7 dependencies
7 dependents
-
The Archimedean property of the constructed rationals proved · kernel-lean · F:rat-le-of-le-add-natdivsucc C:archimedean-property 10 dependencies
9 dependents
-
1 dependencies
37 dependents
-
6 dependencies
32 dependents
-
1 dependencies
16 dependents
-
The rational order is reflexive proved · kernel-lean · F:rat-le-refl C:order-relation 1 dependencies
104 dependents
-
The rational order is total proved · kernel-lean · F:rat-le-total C:total-order 1 dependencies
2 dependents
-
The rational order is transitive proved · kernel-lean · F:rat-le-trans C:transitivity 6 dependencies
100 dependents
-
The leading-index scan reads nothing but its own row proved · kernel-lean · F:rat-leading-index-congr-row 1 dependencies
1 dependents
-
A zero row's leading index is the column count proved · kernel-lean · F:rat-leading-index-eq-cols-of-zero-row 3 dependencies
1 dependents
-
3 dependencies
5 dependents
-
2 dependencies
1 dependents
-
6 dependencies
1 dependents
-
Multiplication distributes over addition on the rationals proved · kernel-lean · F:rat-left-distrib C:distributivity 11 dependencies
46 dependents
-
1 dependencies
13 dependents
-
5 dependencies
1 dependents
-
Rational order: le followed by lt gives lt proved · kernel-lean · F:rat-lt-of-le-of-lt 7 dependencies
6 dependents
-
7 dependencies
8 dependents
-
3 dependencies
0 dependents
-
6 dependencies
1 dependents
-
6 dependencies
0 dependents
-
The rational order is trichotomous proved · kernel-lean · F:rat-lt-trichotomy C:total-order 2 dependencies
4 dependents
-
2 dependencies
1 dependents
-
3 dependencies
1 dependents
-
1 dependencies
2 dependents
-
6 dependencies
1 dependents
-
5 dependencies
1 dependents
-
3 dependencies
1 dependents
-
3 dependencies
1 dependents
-
10 dependencies
0 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
7 dependencies
5 dependents
-
1 dependencies
11 dependents
-
7 dependencies
6 dependents
-
2 dependencies
3 dependents
-
2 dependencies
3 dependents
-
0 dependencies
1 dependents
-
3 dependencies
1 dependents
-
3 dependencies
2 dependents
-
1 dependencies
2 dependents
-
3 dependencies
1 dependents
-
Multiplication on the rationals is associative proved · kernel-lean · F:rat-mul-assoc C:associativity 7 dependencies
37 dependents
-
Multiplication on the rationals is commutative proved · kernel-lean · F:rat-mul-comm C:commutativity 5 dependencies
81 dependents
-
3 dependencies
9 dependents
-
10 dependencies
0 dependents
-
Every nonzero rational has a multiplicative inverse proved · kernel-lean · F:rat-mul-inv-cancel-of-ne-zero C:multiplicative-inverse 3 dependencies
12 dependents
-
A negative rational times its inverse is one proved · kernel-lean · F:rat-mul-inv-cancel-of-neg 16 dependencies
1 dependents
-
A positive rational times its inverse is one proved · kernel-lean · F:rat-mul-inv-cancel 13 dependencies
14 dependents
-
2 dependencies
1 dependents
-
11 dependencies
19 dependents
-
2 dependencies
10 dependents
-
4 dependencies
2 dependents
-
4 dependencies
37 dependents
-
9 dependencies
7 dependents
-
One is a right identity for rational multiplication proved · kernel-lean · F:rat-mul-one C:identity-element 4 dependencies
44 dependents
-
11 dependencies
4 dependents
-
Rational multiplication renormalises proved · kernel-lean · F:rat-mul-renormalises C:rational-arithmetic 1 dependencies
2 dependents
-
7 dependencies
6 dependents
-
A scalar factors out of a rational sumRange proved · kernel-lean · F:rat-mul-sumrange C:summation 2 dependencies
9 dependents
-
Zero absorbs rational multiplication proved · kernel-lean · F:rat-mul-zero C:zero 7 dependencies
25 dependents
-
1 dependencies
1 dependents
-
3 dependencies
1 dependents
-
3 dependencies
1 dependents
-
15 dependencies
1 dependents
-
Bishop's natural sampling indices are closed under composition proved · kernel-lean · F:rat-nat-index-compose C:index-arithmetic 5 dependencies
5 dependents
-
3 dependencies
3 dependents
-
2 dependencies
1 dependents
-
Rational division by a fixed successor denominator adds numerators proved · kernel-lean · F:rat-natdivsucc-add C:rational-arithmetic 7 dependencies
116 dependents
-
10 dependencies
22 dependents
-
5 dependencies
42 dependents
-
natDivSucc is monotone in its numerator proved · kernel-lean · F:rat-natdivsucc-le-add-left 5 dependencies
36 dependents
-
1/(n+1) is at most 1 proved · kernel-lean · F:rat-natdivsucc-le-one 5 dependencies
5 dependents
-
A deeper Bishop sampling index reads back to a coarser bound proved · kernel-lean · F:rat-natdivsucc-le-scaled C:rational-arithmetic 7 dependencies
24 dependents
-
13 dependencies
3 dependents
-
6 dependencies
54 dependents
-
9 dependencies
17 dependents
-
5 dependencies
45 dependents
-
0 dependencies
0 dependents
-
2 dependencies
19 dependents
-
5 dependencies
14 dependents
-
4 dependencies
5 dependents
-
1 dependencies
2 dependents
-
Negation reverses the rational order proved · kernel-lean · F:rat-neg-le-neg C:order-relation 6 dependencies
68 dependents
-
4 dependencies
0 dependents
-
11 dependencies
1 dependents
-
2 dependencies
23 dependents
-
Double negation cancels on the rationals proved · kernel-lean · F:rat-neg-neg C:additive-inverse 2 dependencies
32 dependents
-
Negating a nonnegative rational gives a nonpositive one proved · kernel-lean · F:rat-neg-nonpos-of-nonneg C:non-negativity 2 dependencies
16 dependents
-
Negating a rational difference swaps its operands proved · kernel-lean · F:rat-neg-sub C:additive-inverse 3 dependencies
48 dependents
-
2 dependencies
16 dependents
-
2 dependencies
17 dependents
-
7 dependencies
13 dependents
-
Rat.normalize respects cross-multiplication equality proved · kernel-lean · F:rat-normalize-congr C:congruence 6 dependencies
22 dependents
-
5 dependencies
37 dependents
-
6 dependencies
18 dependents
-
The rational smart constructor normalises proved · kernel-lean · F:rat-normalize-reduces C:rational-numbers 1 dependencies
2 dependents
-
1 dependencies
1 dependents
-
2 dependencies
0 dependents
-
0 dependencies
1 dependents
-
3 dependencies
2 dependents
-
2 dependencies
2 dependents
-
0 dependencies
2 dependents
-
2 dependencies
1 dependents
-
9 dependencies
0 dependents
-
12 dependencies
0 dependents
-
2 dependencies
2 dependents
-
5 dependencies
1 dependents
-
4 dependencies
1 dependents
-
0 dependencies
4 dependents
-
1 dependencies
4 dependents
-
Row-echelon form implies the pivot section proved · kernel-lean · F:rat-pivot-section-of-is-echelon 4 dependencies
3 dependents
-
3 dependencies
0 dependents
-
5 dependencies
1 dependents
-
3 dependencies
0 dependents
-
Rational polynomial evaluation unfolds one degree at a time proved · kernel-lean · F:rat-polyeval-succ C:polynomial-evaluation 0 dependencies
1 dependents
-
0 dependencies
1 dependents
-
3 dependencies
1 dependents
-
5 dependencies
1 dependents
-
3 dependencies
1 dependents
-
2 dependencies
0 dependents
-
0 dependencies
3 dependents
-
0 dependencies
1 dependents
-
2 dependencies
0 dependents
-
12 dependencies
0 dependents
-
2 dependencies
1 dependents
-
7 dependencies
3 dependents
-
Row rank equals column rank over the rationals proved · kernel-lean · F:rat-rank-eq-rank-cols 2 dependencies
2 dependents
-
2 dependencies
1 dependents
-
3 dependencies
0 dependents
-
1 dependencies
1 dependents
-
2 dependencies
1 dependents
-
3 dependencies
0 dependents
-
2 dependencies
4 dependents
-
3 dependencies
0 dependents
-
10 dependencies
1 dependents
-
4 dependencies
0 dependents
-
0 dependencies
3 dependents
-
2 dependencies
19 dependents
-
5 dependencies
0 dependents
-
Gaussian elimination lands in row-echelon form proved · kernel-lean · F:rat-row-echelon-is-echelon 26 dependencies
1 dependents
-
5 dependencies
0 dependents
-
1 dependencies
0 dependents
-
4 dependencies
1 dependents
-
3 dependencies
18 dependents
-
A rational square is never negative proved · kernel-lean · F:rat-sq-nonneg C:non-negativity 9 dependencies
10 dependents
-
3 dependencies
0 dependents
-
The error of a rational sum is the sum of the errors proved · kernel-lean · F:rat-sub-add-add C:subtraction 3 dependencies
14 dependents
-
Rational subtraction telescopes proved · kernel-lean · F:rat-sub-add-sub C:telescoping-sum 3 dependencies
42 dependents
-
6 dependencies
29 dependents
-
8 dependencies
4 dependents
-
6 dependencies
2 dependents
-
4 dependencies
10 dependents
-
2 dependencies
3 dependents
-
A rational minus itself is zero proved · kernel-lean · F:rat-sub-self 1 dependencies
15 dependents
-
2 dependencies
1 dependents
-
5 dependencies
1 dependents
-
2 dependencies
2 dependents
-
2 dependencies
6 dependents
-
2 dependencies
4 dependents
-
sumRange respects pointwise-equal summands proved · kernel-lean · F:rat-sumrange-congr 0 dependencies
28 dependents
-
9 dependencies
1 dependents
-
3 dependencies
3 dependents
-
4 dependencies
2 dependents
-
3 dependencies
1 dependents
-
2 dependencies
0 dependents
-
3 dependencies
1 dependents
-
4 dependencies
3 dependents
-
6 dependencies
1 dependents
-
2 dependencies
1 dependents
-
Summing over a range unfolds one step at the top proved · kernel-lean · F:rat-sumrange-succ C:summation 0 dependencies
1 dependents
-
2 dependencies
3 dependents
-
0 dependencies
1 dependents
-
4 dependencies
0 dependents
-
10 dependencies
0 dependents
-
0 dependencies
0 dependents
-
8 dependencies
2 dependents
-
2 dependencies
1 dependents
-
13 dependencies
3 dependents
-
16 dependencies
1 dependents
-
6 dependencies
1 dependents
-
2 dependencies
3 dependents
-
2 dependencies
0 dependents
-
4 dependencies
2 dependents
-
1 dependencies
2 dependents
-
6 dependencies
2 dependents
-
14 dependencies
2 dependents
-
The weak law of large numbers over the constructed rationals proved · kernel-lean · F:rat-weak-law-of-large-numbers C:law-of-large-numbers 1 dependencies
1 dependents
-
Zero is a left identity for rational addition proved · kernel-lean · F:rat-zero-add C:identity-element 2 dependencies
36 dependents
-
6 dependencies
2 dependents
-
A natural-indexed rational division is never negative proved · kernel-lean · F:rat-zero-le-natdivsucc C:non-negativity 7 dependencies
130 dependents
-
1 dependencies
11 dependents
-
ℚ is a field: Rat.inv is proved to invert, at zero trusted declarations proved · kernel-lean · F:rationals-are-a-field-axiom-free C:rational-numbersC:ordered-field 0 dependencies
1 dependents
-
3 dependencies
4 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
The constructed reals carry max, min and a total absolute value, built with no index shift and no decision procedure proved · kernel-lean · F:real-lattice-is-constructed-axiom-free C:real-numbersC:constructive-analysisC:order-theory 1 dependencies
0 dependents
-
The binary propositional resolution rule is sound proved · smt-term-level · F:resolution-rule-sound C:inference-ruleC:soundnessC:satisfiability +1 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
2 dependencies
1 dependents
-
The optimal sorting network on 3 channels has exactly 3 comparators proved · smt-clausal · F:sorting-network-optimal-size-n3 C:sorting-algorithm 0 dependencies
0 dependents
-
The optimal sorting network on 4 channels has exactly 5 comparators proved · smt-clausal · F:sorting-network-optimal-size-n4 C:sorting-algorithm 0 dependencies
0 dependents
-
The optimal sorting network on 5 channels has exactly 9 comparators proved · smt-clausal · F:sorting-network-optimal-size-n5 C:sorting-algorithm 0 dependencies
0 dependents
-
The optimal sorting network on 6 channels has exactly 12 comparators proved · smt-clausal · F:sorting-network-optimal-size-n6 C:sorting-algorithm 0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
3 dependencies
1 dependents
-
4 dependencies
0 dependents
-
0 dependencies
1 dependents
-
2 dependencies
0 dependents
-
0 dependencies
3 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
6 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
3 dependents
-
0 dependencies
2 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
1 dependencies
1 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
1 dependents
-
2 dependencies
2 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
0 dependents
-
2 dependencies
0 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
2 dependencies
1 dependents
-
2 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
1 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
0 dependents
-
0 dependencies
5 dependents
-
2 dependencies
3 dependents
-
0 dependencies
0 dependents
-
1 dependencies
1 dependents
-
1 dependencies
0 dependents
-
1 dependencies
1 dependents
-
1 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
1 dependencies
3 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
0 dependencies
0 dependents
-
The Tseitin clauses for an AND gate define the gate proved · smt-term-level · F:tseitin-and-gate C:satisfiabilityC:logical-equivalenceC:formal-proof-checking 0 dependencies
0 dependents
-
Twin prime conjecture conjectured · route not assigned · F:twin-prime-unbounded C:twin-prime-conjectureC:prime-numberC:prime-gap 0 dependencies
0 dependents
-
The k-weighted binomial row sum proved · cas-certificate · F:weighted-binomial-row-sum 0 dependencies
0 dependents
-
0 dependencies
2 dependents
-
21 dependencies
0 dependents
-
Exclusive-or is associative proved · smt-term-level · F:xor-associative C:exclusive-orC:associativity-abstractC:logical-connective 0 dependencies
0 dependents
